Ebook: Software Specification Methods: An Overview Using a Case Study

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 volume 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 and LOTOS.
Most specification courses tend to focus on 1 or 2 key techniques and to have a theoretical bias; this book provides a basic overview of the main methods, and has a practical focus that allows the reader to apply their knowledge to real-life situations. It will prove essential reading for all industrial and commercial practitioners who need to expand their knowledge of software specification methods.

---

This volume 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 and LOTOS.
Most specification courses tend to focus on 1 or 2 key techniques and to have a theoretical bias; this book provides a basic overview of the main methods, and has a practical focus that allows the reader to apply their knowledge to real-life situations. It will prove essential reading for all industrial and commercial practitioners who need to expand their knowledge of software specification methods.
Content:
Front Matter....Pages I-XXIII
Front Matter....Pages 1-1
Z: A Formal Specification Notation....Pages 3-19
SAZ: SSADM Version 4 and Z....Pages 21-38
B: A Model-Based Method Using Generalised Substitutions....Pages 39-55
From OMT Diagrams to B Specifications....Pages 57-77
Front Matter....Pages 79-79
Action Systems: A Method Combining State-Based and Event-Based Specification....Pages 81-96
Using UML with a Behaviour-Driven Method....Pages 97-112
VHDL: A Hardware Description Language and its Simulation Semantics....Pages 113-130
Estelle: A Formal Description Technique....Pages 131-145
SDL: A Language Based on Extended Finite State Machines with Abstract Data Types....Pages 147-164
(E)-Lotos: (Enhanced) Language of Temporal Ordering Specification....Pages 165-190
Specifying a Cleanroom Black Box Using JSD....Pages 191-205
Front Matter....Pages 207-207
Algebraic Specification in Casl ....Pages 209-224
An Abstract and Constructive Specification in Coq....Pages 225-240
Petri Nets: A Graphical Tool for System Modelling and Analysis....Pages 241-257
Using Petri Nets and Objects: A Formal yet Expressive Approach....Pages 259-278
Back Matter....Pages 279-286

---

This volume 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 and LOTOS.
Most specification courses tend to focus on 1 or 2 key techniques and to have a theoretical bias; this book provides a basic overview of the main methods, and has a practical focus that allows the reader to apply their knowledge to real-life situations. It will prove essential reading for all industrial and commercial practitioners who need to expand their knowledge of software specification methods.
Content:
Front Matter....Pages I-XXIII
Front Matter....Pages 1-1
Z: A Formal Specification Notation....Pages 3-19
SAZ: SSADM Version 4 and Z....Pages 21-38
B: A Model-Based Method Using Generalised Substitutions....Pages 39-55
From OMT Diagrams to B Specifications....Pages 57-77
Front Matter....Pages 79-79
Action Systems: A Method Combining State-Based and Event-Based Specification....Pages 81-96
Using UML with a Behaviour-Driven Method....Pages 97-112
VHDL: A Hardware Description Language and its Simulation Semantics....Pages 113-130
Estelle: A Formal Description Technique....Pages 131-145
SDL: A Language Based on Extended Finite State Machines with Abstract Data Types....Pages 147-164
(E)-Lotos: (Enhanced) Language of Temporal Ordering Specification....Pages 165-190
Specifying a Cleanroom Black Box Using JSD....Pages 191-205
Front Matter....Pages 207-207
Algebraic Specification in Casl ....Pages 209-224
An Abstract and Constructive Specification in Coq....Pages 225-240
Petri Nets: A Graphical Tool for System Modelling and Analysis....Pages 241-257
Using Petri Nets and Objects: A Formal yet Expressive Approach....Pages 259-278
Back Matter....Pages 279-286
....