Software Specification Methods

by Habrias, Henri; Frappier, Marc

• ISBN13: 9781905209347
• ISBN10: 1905209347
• Edition: 1st
• Format: Hardcover
• Copyright: 2006-05-05
• Publisher: Wiley-ISTE
• More Book Details

Summary

This title provides a clear overview of the main methods, and has a practical focus that allows the reader to apply their knowledge to real-life situations. The following are just some of the techniques covered: UML, Z, TLA+, SAZ, B, OMT, VHDL, Estelle, SDL and LOTOS.

Author Biography

Henri Habrias, University of Nantes, France

Marc Frappier, University of Sherbrooke, Canada

Table of Contents

Preface	vii
List of Contributors	xxiii
Part I State-Based Approaches	1	(136)
1 Z	3	(18)
Jonathan P. BOWEN
1.1 Overview of the Z notation	3	(2)
1.1.1 The process of producing a Z specification	4	(1)
1.2 Analysis and specification of case 1	5	(8)
1.3 Analysis and specification of case 2	13	(3)
1.4 Validation of the specification	16	(2)
1.5 The natural language description of the specifications	18	(1)
1.6 Conclusion	18	(3)
2 SAZ	21	(20)
Fiona POLACK
2.1 Overview of the SAZ method	21	(1)
2.2 Analysis and specification of case 1	22	(6)
2.2.1 Z specification	24	(4)
2.3 Analysis and specification of case 2	28	(9)
2.4 Natural language description of the specifications	37	(1)
2.4.1 Case 1	37	(1)
2.4.2 Case 2	37	(1)
2.5 Conclusions	38	(3)
3 B	41	(18)
Hassan DIAS and Marc FRAPPIER
3.1 Overview of the B notation	41	(1)
3.2 Analysis and specification of case 1	42	(9)
3.2.1 Identifying operations	42	(2)
3.2.2 Defining the state space	44	(2)
3.2.3 Defining the behavior of the invoicing operation	46	(3)
3.2.4 The Productl machine	49	(2)
3.3 Analysis and specification of case 2	51	(3)
3.3.1 Identifying operations	51	(1)
3.3.2 The Product2 machine	51	(1)
3.3.3 The Invoicing2 machine	52	(2)
3.4 Validation of the specification	54	(1)
3.5 The natural language description of the specifications	55	(1)
3.5.1 Case 1	55	(1)
3.5.2 Case 2	55	(1)
3.6 Conclusion	56	(3)
4 From UML Diagrams to 13 Specifications	59	(22)
Régine LALEAU and Amel MAMMAR
4.1 Overview of the method	59	(5)
4.1.1 Summary of the B method	59	(1)
4.1.2 Data specification	60	(1)
4.1.3 Transaction specification	61	(3)
4.2 Specification of case 1	64	(5)
4.2.1 The class diagram and its B representation	64	(2)
4.2.2 Transaction specification	66	(3)
4.3 Specification of case 2	69	(7)
4.3.1 Transactions specification	69	(3)
4.3.2 The formal specification	72	(4)
4.4 Validation	76	(1)
4.5 The natural-language description of specifications	77	(1)
4.5.1 Case 1	77	(1)
4.5.2 Case 2	77	(1)
4.6 Conclusion	77	(4)
5 UML+Z: Augmenting UML with Z	81	(22)
Nuno AMÁLIO, Fiona POLACK, and Susan STEPINEY
5.1 Overview of UML+Z	81	(1)
5.2 Analysis and specification of case 1	82	(8)
5.2.1 UML class model	82	(1)
5.2.2 UML state models	83	(1)
5.2.3 The Z model	84	(4)
5.2.4 Checking model consistency	88	(1)
5.2.5 Validating the model	89	(1)
5.3 Analysis and specification of case 2	90	(11)
5.3.1 Entries of new orders	90	(6)
5.3.2 Cancellation of orders Q	Q4
5.3.3 Entries of quantities into stock	96	(5)
5.4 Natural language description of the specification	101	(1)
5.4.1 Case 1	101	(1)
5.4.2 Case 2	101	(1)
5.5 Conclusion	101	(2)
6 ASM	103	(18)
Egon BÖRGER, Angelo GARGANTINI and Elvinia RICCOBENE
6.1 Overview of the ASM	103	(1)
6.2 Requirements capture and specification of case 1	104	(10)
6.2.1 Identifying the agents	104	(1)
6.2.2 Identifying the states	105	(1)
6.2.3 Identifying static and dynamic parts of the states	105	(2)
6.2.4 Identifying the transitions	107	(4)
6.2.5 Identifying the initial and final states	111	(1)
6.2.6 Exceptions handling and robustness	111	(1)
6.2.7 Identifying the desired properties (validation/verification)	112	(2)
6.3 Requirements capture and specification of case 2	114	(4)
6.4 The natural language description of the specification	118	(1)
6.4.1 Case 1	118	(1)
6.4.2 Case 2	118	(1)
6.5 Conclusion	118	(3)
7 TLA+	121	(16)
Leslie LAMPORT
7.1 Overview of TLA+	121	(3)
7.1.1 TLA	121	(1)
7.1.2 TLA+ versus Z	122	(2)
7.2 A specification of case 2	124	(7)
7.3 The problematic case 1	131	(1)
7.4 Validation of the specification	132	(1)
7.5 Satisfying the specification	133	(1)
7.6 The natural language description	134	(1)
7.7 Conclusion	134	(3)
Part II Event-Based Approaches	137	(138)
8 Action Systems	139	(18)
Jane SINCLAIR
8.1 Overview of action systems	139	(1)
8.2 Analysis and specification of case 1	140	(7)
8.2.1 Modeling the state of the action system	140	(3)
8.2.2 Defining the actions	143	(3)
8.2.3 An action system for case 1	146	(1)
8.3 Analysis and specification of case 2	147	(4)
8.3.1 Modeling the state for case 2	147	(1)
8.3.2 Defining the actions	147	(3)
8.3.3 An action system for case 2	150	(1)
8.4 Verification for action systems	151	(2)
8.5 The natural language description of the specification	153	(1)
8.5.1 Case 1	153	(1)
8.5.2 Case 2	153	(1)
8.6 Conclusion	153	(4)
9 Event B	157	(22)
Dominique CANSELL and Dominique MÉRY
9.1 Introduction	157	(1)
9.2 Analyzing the text of the case study	158	(6)
9.3 Event-based modeling	164	(3)
9.4 Modeling the first event B model Case 1	167	(3)
9.5 Model refinement	170	(1)
9.6 Modeling the second event B model Case 2 by refinement of Case 1	171	(4)
9.7 The natural language description of the event B models	175	(1)
9.8 Conclusion	175	(4)
10 VHDL	179	(18)
Laurence PIERRE
10.1 Overview of VHDL	179	(2)
10.2 Analysis and specification of case 1	181	(5)
10.2.1 Identifying data structures	181	(1)
10.2.2 Identifying operations	182	(4)
10.3 Analysis and specification of case 2	186	(7)
10.4 The natural language description of the specification	193	(1)
10.4.1 Case 1	193	(1)
10.4.2 Case 2	194	(1)
10.5 Conclusion	194	(3)
11 Estelle	197	(18)
Eric LALLET and Jean-Luc RAFFY
11.1 Overview of the FDT Estelle	197	(1)
11.2 Analysis and specification of case 1	198	(6)
11.2.1 Defining the architecture of the specification	198	(2)
11.2.2 Defining the behavior	200	(4)
11.3 Analysis and specification of case 2	204	(6)
11.3.1 Defining the new architecture	204	(1)
11.3.2 Defining the behavior	205	(5)
11.4 Validating the specification	210	(1)
11.5 The natural language description of the specifications	210	(2)
11.5.1 Case 1	210	(1)
11.5.2 Case 2	210	(2)
11.6 JEstelle (Estelle with Java)	212	(1)
11.7 Conclusion	212	(3)
12 SDL	215	(18)
Pascal POIZAT
12.1 Overview of SDL	215	(1)
12.2 Analysis and specification of case 1	216	(9)
12.2.1 System structure	216	(3)
12.2.2 Process graphs	219	(2)
12.2.3 Sort definitions	221	(4)
12.2.4 Comments on the first case study	225	(1)
12.3 Analysis and specification of case 2	225	(5)
12.3.1 System structure	225	(2)
12.3.2 Process graphs	227	(1)
12.3.3 Sort definitions	228	(2)
12.4 The natural language description of the specifications	230	(1)
12.4.1 Case 1	230	(1)
12.4.2 Case 2	230	(1)
12.5 Conclusion	230	(3)
13 E-LOTOS	233	(26)
Kenneth J. TURNER and Mihaela SIGHIREANU
13.1 Overview of the LOTOS notation and method	233	(3)
13.1.1 The LOTOS and E-Lows languages	233	(1)
13.1.2 Requirements capture in LOTOS	234	(2)
13.2 Analysis and specification of case 1	236	(1)
13.2.1 Analysis	236	(1)
13.2.2 Specification	237	(1)
13.3 Analysis and specification of case 2	237	(13)
13.3.1 Analysis	238	(4)
13.3.2 Specification	242	(8)
13.4 Validation and verification of the LOTOS specifications	250	(5)
13.4.1 Validation	250	(1)
13.4.2 Verification	251	(4)
13.5 Natural language description of the specifications	255	(1)
13.5.1 Case 1	255	(1)
13.5.2 Case 2	255	(1)
13.6 Conclusion	255	(4)
14 EB³	259	(16)
Frédéric GERVAIS, Marc FRAPPIER and Richard ST-DENIS
14.1 Introduction	259	(1)
14.2 Analysis and specification of case 1	260	(3)
14.2.1 Entity types and actions	260	(2)
14.2.2 Process expressions	262	(1)
14.2.3 Input-output rules	262	(1)
14.3 Analysis and specification of case 2	263	(8)
14.3.1 Entity types, associations and actions	263	(3)
14.3.2 Process expressions	266	(2)
14.3.3 Input-output rules	268	(1)
14.3.4 Attribute definitions	268	(3)
14.4 The natural language description of the specification	271	(1)
14.4.1 Case 1	271	(1)
14.4.2 Case 2	272	(1)
14.5 Conclusion	272	(3)
Part III Other Formal Approaches	275	(76)
15 CASL	277	(16)
Hubert BAUMEISTER and Didier BERT
15.1 Overview of the CASL notation	277	(1)
15.2 Analysis and specification of case 1	278	(5)
15.3 Analysis and specification of case 2	283	(6)
15.4 Architectural specification	289	(1)
15.5 The natural language description of the specification	290	(1)
15.5.1 Case 1	290	(1)
15.5.2 Case 2	290	(1)
15.6 Conclusion	291	(2)
16 Coq	293	(18)
Philippe CHAVIN and Jean-François MONIN
16.1 Introduction to Coq	293	(1)
16.2 Analysis of the text	294	(2)
16.2.1 Stock and orders	294	(1)
16.2.2 Operations	295	(1)
16.2.3 Requirements on quantities	296	(1)
16.3 A specification for case 1	296	(4)
16.3.1 Basic types	296	(2)
16.3.2 State and operation	298	(1)
16.3.3 Operation "i n voice"	298	(2)
16.4 A specification for case 2	300	(4)
16.4.1 Using general operations over sets	300	(2)
16.4.2 Reference-dependent measure systems	302	(2)
16.5 Experimenting with the specification	304	(2)
16.5.1 Refining	304	(2)
16.6 Running an example	306	(1)
16.7 Rephrasing the text	307	(1)
16.8 Conclusion	308	(3)
17 Petri Nets	311	(18)
Annie CHOQUET-GENIET and Pascal RICHARD
17.1 Overview of Petri nets	311	(1)
17.2 Analysis and specification of case 1	312	(10)
17.2.1 One order with a data/action approach	313	(3)
17.2.2 One order with a structural approach	316	(3)
17.2.3 Several orders	319	(3)
17.3 Analysis and specification of case 2	322	(2)
17.3.1 Entry flow in stocks	322	(1)
17.3.2 Flows of orders	323	(1)
17.4 Validation of the specification	324	(2)
17.5 The natural language description of the specifications	326	(1)
17.5.1 Case 1	326	(1)
17.5.2 Case 2	326	(1)
17.6 Conclusion	326	(3)
18 Petri Nets with Objects	329	(22)
Christophe SIBERTIN-BLANC
18.1 Introduction	329	(1)
18.2 A conceptual framework for the representation of systems	330	(2)
18.3 Case 1	332	(1)
18.4 The system's interface	332	(1)
18.5 The components of the system's structure	333	(2)
18.6 The Entities	335	(3)
18.7 The Operations	338	(1)
18.8 The Actors	339	(1)
18.9 The Control Structure	340	(5)
18.10 Natural language description of the specifications	345	(1)
18.11 Comments about our treatment of the case study	346	(5)
Part IV Comparison and Glossary	351	(60)
19 A Comparison of the Specification Methods	353	(12)
Marc FRAPPIER, Henri HABRIAS and Pascal POIZAT
19.1 Attributes of specification methods	353	(6)
19.1.1 Paradigm	353	(3)
19.1.2 Formality	356	(1)
19.1.3 Graphical representation	357	(1)
19.1.4 Object oriented	357	(1)
19.1.5 Concurrency	357	(1)
19.1.6 Executability	357	(1)
19.1.7 Usage of variables	357	(1)
19.1.8 Non-determinism	357	(1)
19.1.9 Logic	358	(1)
19.1.10 Provability	358	(1)
19.1.11 Model checking	358	(1)
19.1.12 Event inhibition	358	(1)
19.2 A qualitative description of the methods	359	(6)
20 Glossary	365	(46)
Henri HABRIAS, Pascal POIZAT and Marc FRAPPIER
Index	411