This is the only up-to-date survey of specification techniques
Software Specification Methods provides the formal methods practitioner with a survey of the key software specification methods. Each technique is demonstrated using the same case study, an invoicing system, to enable the reader to compare and contrast easily. Among the techniques covered are: UML; Z; SAZ; B; JSD; OMT; VHDL; Estelle; SDL; LOTOS. This book is intended for industrial and commercial practitioners who need to expand their knowledge of software specification methods. This book provides a basic overview of the main methods, with a practical focus which allows readers to apply their knowledge to real-life situations.|Objectives of this Book This book is an introduction to a set of software specification methods. Its tar geted audience are readers who do not wish to read pages of definitions in order to understand the basics of a method. The same case study is used to introduce each method, following a rigorously uniform presentation format. Special care has been devoted to ensure that specifications do not deviate from the case study text. As much as the method allows, what is specified is what appears in the case study text. The benefits are two-fold. First, the reader can easily switch from one method to another, using his knowledge of the case study as a leverage to understand a new method. Second, it becomes easier to compare methods, because the same behavior is specified in each case. Each method presentation follows the same pattern. The concepts are pro gressively introduced when they are needed. To illustrate the specification pro cess, questions that the specifier should raise during the analysis of the case study are stated. Answers are provided as if they were given by an imaginary client. The question/answer process guides the derivation of the specification. Interestingly, the questions raised depend on the method, which is illustrative of the differences between them.
Part I: State-Based Approaches1. Z: A Formal Specification Notation.-2. SAZ: SSADM Version 4 and Z.-3. B: A Model-Based Method Using Generalized Substitutions.- 4. From OMT Diagrams to B Specifications.-Part II: Event-Based Approaches5. Action Systems: A Method Combining State-Based and Event-Based Specification.-6. Using UML with a Behaviour-Driven Method.-7. VHDL: A Hardware Deillegalscription Language and its Simulation Semantics.-8. Estelle: A Formal Deillegalscription Technique.-9. SDL: A Specification and Deillegalscription Language Based on an Extended Finite State Machine Model with Abstract Data Types.-10. (E-)LOTOS: (Enhanced) Language of Temporal Ordering Specification.-11. Specifying a Cleanroom Black Box Using JSD.-Part III: Other Formal Approaches12. Algebraic Specification in CASL.-13. Coq: A Constructive Proof System.-14. Petri Nets: A Graphical Tool for System Modelling and Analysis.-15. Using Petri Nets and Objects: A Formal Yet Expressive Approach.
Objectives of this Book This book is an introduction to a set of software specification methods. Its tar geted audience are readers who do not wish to read pages of definitions in order to understand the basics of a method. The same case study is used to introduce each method, following a rigorously uniform presentation format. Special care has been devoted to ensure that specifications do not deviate from the case study text. As much as the method allows, what is specified is what appears in the case study text. The benefits are two-fold. First, the reader can easily switch from one method to another, using his knowledge of the case study as a leverage to understand a new method. Second, it becomes easier to compare methods, because the same behavior is specified in each case. Each method presentation follows the same pattern. The concepts are pro gressively introduced when they are needed. To illustrate the specification pro cess, questions that the specifier should raise during the analysis of the case study are stated. Answers are provided as if they were given by an imaginary client. The question/answer process guides the derivation of the specification. Interestingly, the questions raised depend on the method, which is illustrative of the differences between them.
I State-Based Approaches.- 1 Z: A Formal Specification Notation.- 2 SAZ: SSADM Version 4 and Z.- 3 B: A Model-Based Method Using Generalised Substitutions.- 4 From OMT Diagrams to B Specifications.- II Event-Based Approaches.- 5 Action Systems: A Method Combining State-Based and Event-Based Specification.- 6 Using UML with a Behaviour-Driven Method.- 7 VHDL: A Hardware Deillegalscription Language and its Simulation Semantics.- 8 Estelle: A Formal Deillegalscription Technique.- 9 SDL: A Language Based on Extended Finite State Machines with Abstract Data Types.- 10 (E)-Lotos: (Enhanced) Language of Temporal Ordering Specification.- 11 Specifying a Cleanroom Black Box Using JSD.- III Other Formal Approaches.- 12 Algebraic Specification in Casl.- 13 An Abstract and Constructive Specification in Coq.- 14 Petri Nets: A Graphical Tool for System Modelling and Analysis.- 15 Using Petri Nets and Objects: A Formal yet Expressive Approach.
Inhaltsverzeichnis
Part I: State-Based Approaches
1. Z: A Formal Specification Notation.-
2. SAZ: SSADM Version 4 and Z.-
3. B: A Model-Based Method Using Generalized Substitutions.- 4. From OMT Diagrams to B Specifications.-
Part II: Event-Based Approaches
5. Action Systems: A Method Combining State-Based and Event-Based Specification.-
6. Using UML with a Behaviour-Driven Method.-
7. VHDL: A Hardware Deillegalscription Language and its Simulation Semantics.-
8. Estelle: A Formal Deillegalscription Technique.-
9. SDL: A Specification and Deillegalscription Language Based on an Extended Finite State Machine Model with Abstract Data Types.-
10. (E-)LOTOS: (Enhanced) Language of Temporal Ordering Specification.-
11. Specifying a Cleanroom Black Box Using JSD.-
Part III: Other Formal Approaches
12. Algebraic Specification in CASL.-
13. Coq: A Constructive Proof System.-
14. Petri Nets: A Graphical Tool for System Modelling and Analysis.-
15. Using Petri Nets and Objects: A Formal Yet Expressive Approach.
Klappentext
Objectives of this Book This book is an introduction to a set of software specification methods. Its tar geted audience are readers who do not wish to read pages of definitions in order to understand the basics of a method. The same case study is used to introduce each method, following a rigorously uniform presentation format. Special care has been devoted to ensure that specifications do not deviate from the case study text. As much as the method allows, what is specified is what appears in the case study text. The benefits are two-fold. First, the reader can easily switch from one method to another, using his knowledge of the case study as a leverage to understand a new method. Second, it becomes easier to compare methods, because the same behavior is specified in each case. Each method presentation follows the same pattern. The concepts are pro gressively introduced when they are needed. To illustrate the specification pro cess, questions that the specifier should raise during the analysis of the case study are stated. Answers are provided as if they were given by an imaginary client. The question/answer process guides the derivation of the specification. Interestingly, the questions raised depend on the method, which is illustrative of the differences between them.
This is the only up-to-date survey of specification techniques
