Software Specification Methods

Henri Habrias, University of Nantes, France Marc Frappier, University of Sherbrooke, Canada

• Preface viiList of Contributors xxiiiPart I State-Based Approaches 11 Z 3Jonathan P. Bowen1.1 Overview of the Z notation 31.1.1 The process of producing a Z specification 41.2 Analysis and specification of case 1 51.3 Analysis and specification of case 2 131.4 Validation of the specification 161.5 The natural language description of the specifications 181.6 Conclusion 182 SAZ 21Fiona Polack2.1 Overview of the SAZ method 212.2 Analysis and specification of case 1 222.2.1 Z specification 242.3 Analysis and specification of case 2 282.4 Natural language description of the specifications 372.4.1 Case 1 372.4.2 Case 2 372.5 Conclusions 383 B 41Hassan Diab and Marc Frappier3.1 Overview of the B notation 413.2 Analysis and specification of case 1 423.2.1 Identifying operations 423.2.2 Defining the state space 443.2.3 Defining the behavior of the invoicing operation 463.2.4 The Product1 machine 493.3 Analysis and specification of case 2 513.3.1 Identifying operations 513.3.2 The Product2 machine 513.3.3 The Invoicing2 machine 523.4 Validation of the specification 543.5 The natural language description of the specifications 553.5.1 Case 1 553.5.2 Case 2 553.6 Conclusion 564 From UML Diagrams to B Specifications 59Régine Laleau and Amel Mammar4.1 Overview of the method 594.1.1 Summary of the B method 594.1.2 Data specification 604.1.3 Transaction specification 614.2 Specification of case 1 644.2.1 The class diagram and its B representation 644.2.2 Transaction specification 664.3 Specification of case 2 694.3.1 Transactions specification 694.3.2 The formal specification 724.4 Validation 764.5 The natural-language description of the specifications 774.5.1 Case 1 774.5.2 Case 2 774.6 Conclusion 775 UML+Z: Augmenting UML with Z 81Nuno Amálio, Fiona Polack, and Susan Stepney5.1 Overview of UML+ Z 815.2 Analysis and specification of case 1 825.2.1 UML class model 825.2.2 UML state models 835.2.3 The Z model 845.2.4 Checking model consistency 885.2.5 Validating the model 895.3 Analysis and specification of case 2 905.3.1 Entries of new orders 905.3.2 Cancellation of orders 945.3.3 Entries of quantities into stock 965.4 Natural language description of the specification 1015.4.1 Case 1 1015.4.2 Case 2 1015.5 Conclusion 1016 ASM 103Egon Börger, Angelo Gargantini and Elvinia Riccobene6.1 Overview of the ASM 1036.2 Requirements capture and specification of case 1 1046.2.1 Identifying the agents 1046.2.2 Identifying the states 1056.2.3 Identifying static and dynamic parts of the states 1056.2.4 Identifying the transitions 1076.2.5 Identifying the initial and final states 1116.2.6 Exceptions handling and robustness 1116.2.7 Identifying the desired properties (validation/verification) 1126.3 Requirements capture and specification of case 2 1146.4 The natural language description of the specification 1186.4.1 Case 1 1186.4.2 Case 2 1186.5 Conclusion 1187 TLA+ 121Leslie Lamport7.1 Overview of TLA+ 1217.1.1 TLA 1217.1.2 TLA+ versus Z 1227.2 A specification of case 2 1247.3 The problematic case 1 1317.4 Validation of the specification 1327.5 Satisfying the specification 1337.6 The natural language description 1347.7 Conclusion 134Part II Event-Based Approaches 1378 Action Systems 139Jane Sinclair8.1 Overview of action systems 1398.2 Analysis and specification of case 1 1408.2.1 Modeling the state of the action system 1408.2.2 Defining the actions 1438.2.3 An action system for case 1 1468.3 Analysis and specification of case 2 1478.3.1 Modeling the state for case 2 1478.3.2 Defining the actions 1478.3.3 An action system for case 2 1508.4 Verification for action systems 1518.5 The natural language description of the specification 1538.5.1 Case 1 1538.5.2 Case 2 1538.6 Conclusion 1539 Event B 157Dominique Cansell and Dominique Méry9.1 Introduction 1579.2 Analyzing the text of the case study 1589.3 Event-based modeling 1649.4 Modeling the first event B model Case 1 1679.5 Model refinement 1709.6 Modeling the second event B model Case 2 by refinement of Case 1 1719.7 The natural language description of the event B models 1759.8 Conclusion 17510 VHDL 179Laurence Pierre10.1 Overview of VHDL 17910.2 Analysis and specification of case 1 18110.2.1 Identifying data structures 18110.2.2 Identifying operations 18210.3 Analysis and specification of case 2 18610.4 The natural language description of the specification 19310.4.1 Case 1 19310.4.2 Case 2 19410.5 Conclusion 19411 Estelle 197Eric Lallett and Jean-Luc Raffy11.1 Overview of the FDT Estelle 19711.2 Analysis and specification of case 1 19811.2.1 Defining the architecture of the specification 19811.2.2 Defining the behavior 20011.3 Analysis and specification of case 2 20411.3.1 Defining the new architecture 20411.3.2 Defining the behavior 20511.4 Validating the specification 21011.5 The natural language description of the specifications 21011.5.1 Case 1 21011.5.2 Case 2 21011.6 JEstelle (Estelle with Java) 21211.7 Conclusion 21212 SDL 215Pascal Poizat12.1 Overview of SDL 21512.2 Analysis and specification of case 1 21612.2.1 System structure 21612.2.2 Process graphs 21912.2.3 Sort definitions 22112.2.4 Comments on the first case study 22512.3 Analysis and specification of case 2 22512.3.1 System structure 22512.3.2 Process graphs 22712.3.3 Sort definitions 22812.4 The natural language description of the specifications 23012.4.1 Case 1 23012.4.2 Case 2 23012.5 Conclusion 23013 E-LOTOS 233Kenneth J. Turner and Mihaela Sighireanu13.1 Overview of the LOTOS notation and method 23313.1.1 The LOTOS and E-LOTOS languages 23313.1.2 Requirements capture in LOTOS 23413.2 Analysis and specification of case 1 23613.2.1 Analysis 23613.2.2 Specification 23713.3 Analysis and specification of case 2 23713.3.1 Analysis 23813.3.2 Specification 24213.4 Validation and verification of the LOTOS specifications 25013.4.1 Validation 25013.4.2 Verification 25113.5 Natural language description of the specifications 25513.5.1 Case 1 25513.5.2 Case 2 25513.6 Conclusion 25514 EB3 259Frédéric Gervais, Marc Frappier and Richard St-Denis14.1 Introduction 25914.2 Analysis and specification of case 1 26014.2.1 Entity types and actions 26014.2.2 Process expressions 26214.2.3 Input-output rules 26214.3 Analysis and specification of case 2 26314.3.1 Entity types, associations and actions 26314.3.2 Process expressions 26614.3.3 Input-output rules 26814.3.4 Attribute definitions 26814.4 The natural language description of the specification 27114.4.1 Case 1 27114.4.2 Case 2 27214.5 Conclusion 272Part III Other Formal Approaches 27515 CASL 277Hubert Baumeister and Didier Bert15.1 Overview of the CASL notation 27715.2 Analysis and specification of case 1 27815.3 Analysis and specification of case 2 28315.4 Architectural specification 28915.5 The natural language description of the specification 29015.5.1 Case 1 29015.5.2 Case 2 29015.6 Conclusion 29116 Coq 293Philippe Chavin and Jean-Francǫis Monin16.1 Introduction to Coq 29316.2 Analysis of the text 29416.2.1 Stock and orders 29416.2.2 Operations 29516.2.3 Requirements on quantities 29616.3 A specification for case1 29616.3.1 Basic types 29616.3.2 State and operation 29816.3.3 Operation “invoice” 29816.4 A specification for case2 30016.4.1 Using general operations over sets 30016.4.2 Reference-dependent measure systems 30216.5 Experimenting with the specification 30416.5.1 Refining 30416.6 Running an example 30616.7 Rephrasing the text 30716.8 Conclusion 30817 Petri Nets 311Annie Choquet-Geniet and Pascal Richard17.1 Overview of Petrinets 31117.2 Analysis and specification of case 1 31217.2.1 One order with a data/action approach 31317.2.2 One order with a structural approach 31617.2.3 Several orders 31917.3 Analysis and specification of case 2 32217.3.1 Entry flow in stocks 32217.3.2 Flows of orders 32317.4 Validation of the specification 32417.5 The natural language description of the specifications 32617.5.1 Case 1 32617.5.2 Case 2 32617.6 Conclusion 32618 Petri Nets with Objects 329Christophe Sibertin-Blanc18.1 Introduction 32918.2 A conceptual framework for the representation of systems 33018.3 Case 1 33218.4 The system’s interface 33218.5 The components of the system’s structure 33318.6 The Entities 33518.7 The Operations 33818.8 The Actors 33918.9 The Control Structure 34018.10 Natural language description of the specifications 34518.11 Comments about our treatment of the case study 346Part IV Comparison and Glossary 35119 A Comparison of the Specification Methods 353Marc Frappier, Henri Habrias and Pascal Poizat19.1 Attributes of specification methods 35319.1.1 Paradigm 35319.1.2 Formality 35619.1.3 Graphical representation 35719.1.4 Object oriented 35719.1.5 Concurrency 35719.1.6 Executability 35719.1.7 Usage of variables 35719.1.8 Non-determinism 35719.1.9 Logic 35819.1.10 Provability 35819.1.11 Model checking 35819.1.12 Event inhibition 35819.2 A qualitative description of the methods 35920 Glossary 365Henri Habrias, Pascal Poizat and Marc FrappierIndex 411