Details

Software Specification Methods

, Band 106 1. Aufl.

von: Henri Habrias, Marc Frappier
160,99 €
Verlag:	Wiley
Format:	PDF
Veröffentl.:	05.01.2010
ISBN/EAN:	9780470394656
Sprache:	englisch
Anzahl Seiten:	418

In den Warenkorb

Als Gutschein

DRM-geschütztes eBook, Sie benötigen z.B. Adobe Digital Editions und eine Adobe ID zum Lesen.

Beschreibungen

Titelbeschreibung

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.

Inhaltsverzeichnis

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