Software Specification Methods

1. Front Matter

   Pages I-XXIII

   PDF

2. State-Based Approaches

   1. Front Matter

      Pages 1-1

      PDF

   2. Z: A Formal Specification Notation

      • Jonathan P. Bowen

      Pages 3-19

   3. SAZ: SSADM Version 4 and Z

      • Fiona Polack

      Pages 21-38

   4. B: A Model-Based Method Using Generalised Substitutions

      • Hassan Diab, Marc Frappier

      Pages 39-55

   5. From OMT Diagrams to B Specifications

      • Philippe Facon, Régine Laleau, Hong Phuong Nguyen

      Pages 57-77

3. Event-Based Approaches

   1. Front Matter

      Pages 79-79

      PDF

   2. Action Systems: A Method Combining State-Based and Event-Based Specification

      • Jane Sinclair

      Pages 81-96

   3. Using UML with a Behaviour-Driven Method

      • Sophie Dupuy, Agnès Front-Conte, Christophe Saint-Marcel

      Pages 97-112

   4. VHDL: A Hardware Description Language and its Simulation Semantics

      • Laurence Pierre

      Pages 113-130

   5. Estelle: A Formal Description Technique

      • Eric Lallet, Jean-Luc Raffy

      Pages 131-145

   6. SDL: A Language Based on Extended Finite State Machines with Abstract Data Types

      • P. Poizat

      Pages 147-164

   7. (E)-Lotos: (Enhanced) Language of Temporal Ordering Specification

      • Kenneth J. Turner, Mihaela Sighireanu

      Pages 165-190

   8. Specifying a Cleanroom Black Box Using JSD

      • Marc Frappier, Richard St-Denis

      Pages 191-205

4. Other Formal Approaches

   1. Front Matter

      Pages 207-207

      PDF

   2. Algebraic Specification in Casl

      • Hubert Baumeister, Didier Bert

      Pages 209-224

   3. An Abstract and Constructive Specification in Coq

      • Philippe Chavin, Jean-François Monin

      Pages 225-240

   4. Petri Nets: A Graphical Tool for System Modelling and Analysis

      • Annie Choquet-Geniet, Pascal Richard

      Pages 241-257

   5. Using Petri Nets and Objects: A Formal yet Expressive Approach

      • Christophe Sibertin-Blanc

      Pages 259-278

5. Back Matter

   Pages 279-286

   PDF

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.

• Clean
• Coq
• Language of Temporal Ordering Specification
• Software Engineering
• Specification and Description Language
• formal methods
• formal specification
• language
• modeling
• petri net
• semantics
• simulation
• software
• structured analysis
• structured de

• Département de Mathématiques et d’Informatique, Université de Sherbrooke, Sherbrooke, Canada

  Marc Frappier

• IRIN, Nantes Cedex 03, France

  Henri Habrias

• Institut Universitaire de Technologie, Department informatique, Université de Nantes, Nantes Cedex 03, France

  Henri Habrias

• Institut de Recherches en Informatique de Nantes, Université de Nantes, Nantes Cedex 03, France

  Henri Habrias

Policies and ethics