Software Specification Methods

by Frappier, Marc; Habrias, Henri

• ISBN13: 9781852333539
• ISBN10: 1852333537
• eBook ISBN(s): 9781447107019
• Format: Paperback
• Copyright: 2000-11-01
• Publisher: Springer Nature
• More Book Details
• Purchase Benefits

Summary

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.

Table of Contents

List of Contributors	xxi
Part I State-Based Approaches
Z: A Formal Specification Notation	3	(18)
Jonathan P. Bowen
Overview of the Z Notation	3	(2)
The Process of Producing a Z Specification	3	(2)
Analysis and Specification of Case 1	5	(8)
Analysis and Specification of Case 2	13	(3)
Validation of the Specification	16	(2)
The Natural Language Description of the Specifications	18	(1)
Conclusion	18	(3)
SAZ: SSADM Version 4 and Z	21	(18)
Fiona Polack
Overview of the SAZ Method	21	(1)
Analysis and Specification of Case 1	22	(5)
Z Specification	24	(3)
Analysis and Specification of Case 2	27	(9)
Natural Language Description of the Specifications	36	(1)
Case 1	36	(1)
Case 2	36	(1)
Conclusions	37	(2)
B: A Model-Based Method Using Generalised Substitutions	39	(18)
Hassan Diab
Marc Frappier
Overview of the B Notation	39	(1)
Analysis and Specification of Case 1	40	(9)
Identifying Operations	40	(1)
Defining the State Space	41	(3)
Defining the Behaviour of the Invoicing Operation	44	(2)
The Product1 Machine	46	(3)
Analysis and Specification of Case 2	49	(3)
Identifying Operations	49	(1)
The Product2 Machine	49	(1)
The Invoicing2 Machine	50	(2)
Validation of the Specification	52	(1)
The Natural Language Description of the Specifications	53	(1)
Case 1	53	(1)
Case 2	53	(1)
Conclusion	54	(3)
From OMT Diagrams to B Specifications	57	(24)
Philippe Facon
Regine Laleau
Hong Phuong Nguyen
Overview of the Method	57	(4)
The Semi-Formal Specification	57	(2)
The Formal Specification	59	(2)
Specification of Case 1	61	(5)
Object Diagram	61	(1)
Scenarios and State/Transition Diagrams	62	(2)
The Formal Specification	64	(2)
Specification of Case 2	66	(8)
Scenarios and State/Transition Diagrams	67	(3)
The Formal Specification	70	(4)
Validation	74	(1)
The Natural Language Description of the Specifications	75	(1)
Case 1	75	(1)
Case 2	75	(1)
Conclusion	76	(5)
Part II Event-Based Approaches
Action Systems: A Method Combining State-Based and Event-Based Specification	81	(16)
Jane Sinclair
Overview of Action Systems	81	(1)
Analysis and Specification of Case 1	82	(6)
Modelling the State of the Action System	82	(2)
Defining the Actions	84	(3)
An Action System for Case 1	87	(1)
Analysis and Specification of Case 2	88	(3)
Modelling the State for Case 2	88	(1)
Defining the Actions	89	(2)
An Action System for Case 2	91	(1)
Verification for Action Systems	91	(3)
The Natural Language Description of the Specification	94	(1)
Case 1	94	(1)
Case 2	94	(1)
Conclusion	95	(2)
Using UML with a Behaviour-Driven Method	97	(16)
Sophie Dupuy
Agnes Front-Conte
Christophe Saint-Marcel
Overview of the UML Notation and of the CSO Method	97	(1)
Case 1	98	(5)
Requirements Capture	98	(1)
Analysis and Design	99	(4)
Case 2	103	(8)
Requirements Capture	103	(3)
Analysis and Design Phase	106	(5)
Natural Language Description of the UML Specifications	111	(1)
Case 1	111	(1)
Case 2	111	(1)
Conclusion	111	(2)
VHDL: A Hardware Description Language and its Simulation Semantics	113	(18)
Laurence Pierre
Overview of VHDL	113	(2)
Analysis and Specification of Case 1	115	(5)
Identifying Data Structures	115	(1)
Identifying Operations	116	(4)
Analysis and Specification of Case 2	120	(8)
The Natural Language Description of the Specification	128	(1)
Case 1	128	(1)
Case 2	128	(1)
Conclusion	129	(2)
Estelle: A Formal Description Technique	131	(16)
Eric Lallet
Jean-Luc Raffy
Overview of the FDT Estelle	131	(1)
Analysis and Specification of Case 1	131	(6)
Defining the Architecture of the Specification	132	(2)
Defining the Behaviour	134	(3)
Analysis and Specification of Case 2	137	(6)
Defining the New Architecture	138	(1)
Defining the Behaviour	139	(4)
Validating the Specification	143	(1)
The Natural Language Description of the Specifications	143	(1)
Case 1	143	(1)
Case 2	144	(1)
Conclusion	144	(3)
SDL: A Language Based on Extended Finite State Machines with Abstract Data Types	147	(18)
P. Poizat
Overview of SDL	147	(1)
Analysis and Specification of Case 1	148	(9)
System Structure	148	(2)
Process Graphs	150	(3)
Sort Definitions	153	(4)
Comments on the First Case Study	157	(1)
Analysis and Specification of Case 2	157	(5)
System Structure	157	(2)
Process Graphs	159	(1)
Sort Definitions	160	(2)
The Natural Language Description of the Specifications	162	(1)
Case 1	162	(1)
Case 2	162	(1)
Conclusion	162	(3)
(E)-Lotos: (Enhanced) Language of Temporal Ordering Specification	165	(26)
Kenneth J. Turner
Mihaela Sighireanu
Overview of the Lotos Notation and Method	165	(3)
The Lotos and E-Lotos Languages	165	(1)
Requirements Capture in Lotos	166	(2)
Analysis and Specification of Case 1	168	(2)
Analysis	168	(1)
Specification	169	(1)
Analysis and Specification of Case 2	170	(12)
Analysis	170	(4)
Specification	174	(8)
Validation and Verification of the Lotos Specifications	182	(4)
Validation	182	(1)
Verification	183	(3)
Natural Language Description of the Specifications	186	(1)
Case 1	187	(1)
Case 2	187	(1)
Conclusion	187	(4)
Specifying a Cleanroom Black Box Using JSD	191	(18)
Marc Frappier
Richard St-Denis
Overview of the Method	191	(1)
Analysis and Specification of Case 1	192	(3)
Declaration of Input-Output Space and Entity Types	192	(2)
Definition of Global Constraints	194	(1)
Specification of Input-Output Behaviour	195	(1)
Analysis and Specification of Case 2	195	(8)
Declaration of Input-Output Space and Entity Types	195	(2)
Description of Individual Behaviours of Entities	197	(3)
Definition of Global Constraints	200	(2)
Specification of Input-Output Behaviour	202	(1)
The Natural Language Description of the Specification	203	(1)
Case 1	203	(1)
Case 2	203	(1)
Conclusion	204	(5)
Part III Other Formal Approaches
Algebraic Specification in CASL	209	(16)
Hubert Baumeister
Didier Bert
Overview of the CASL Notation	209	(1)
Analysis and Specification of Case 1	210	(5)
Analysis and Specification of Case 2	215	(6)
Architectural Specification	221	(1)
The Natural Language Description of the Specification	222	(1)
Case 1	222	(1)
Case 2	223	(1)
Conclusion	223	(2)
References	224	(1)
An Abstract and Constructive Specification in Coq	225	(16)
Philippe Chavin
Jean-Francois Monin
Introduction to Coq	225	(1)
Terms Analysis	226	(2)
Stock and Orders	226	(1)
Operations	227	(1)
Requirements on Quantities	227	(1)
A Specification for Case 1	228	(4)
Basic Types	228	(2)
State and Operation	230	(1)
Operation ``invoice''	230	(2)
A Specification for Case 2	232	(4)
Using General Operations over Sets	232	(2)
Reference-Dependent Measure Systems	234	(2)
Experimenting with the Specification	236	(3)
Refining	236	(2)
Running an Example	238	(1)
Terms Rephrasing	239	(1)
Conclusion	240	(1)
Petri Nets: A Graphical Tool for System Modelling and Analysis	241	(18)
Annie Choquet-Geniet
Pascal Richard
Overview of Petri Nets	241	(2)
Analysis and Specification of Case 1	243	(9)
One Order with a Data/Action Approach	243	(4)
One Order with a Structural Approach	247	(2)
Several Orders	249	(3)
Analysis and Specification of Case 2	252	(1)
Entry Flow in Stocks	252	(1)
Flows of Orders	253	(1)
Validation of the Specification	253	(3)
The Natural Language Description of the Specifications	256	(1)
Case 1	256	(1)
Case 2	256	(1)
Conclusion	256	(3)
Using Petri Nets and Objects: A Formal yet Expressive Approach	259	(20)
Christophe Sibertin-Blanc
Introduction	259	(1)
A Conceptual Framework for the Representation of Systems	260	(2)
Case 1	262	(1)
The System's Interface	262	(1)
The Components of the System's Structure	262	(2)
The Entities	264	(4)
The Operations	268	(1)
The Actors	269	(1)
The Control Structure	270	(5)
Natural Language Description of the Specifications	275	(1)
Remarks about the Treatment of the Case Study	275	(4)
Index	279