Skip to main content
SpringerLink
Log in
Book cover

Software Specification Methods

An Overview Using a Case Study

  • Book
  • © 2001

Overview

Editors:
  1. Marc Frappier

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

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Henri Habrias

    1. IRIN, Nantes Cedex 03, France
      Institut Universitaire de Technologie, Department informatique, Université de Nantes, Nantes Cedex 03, France
      Institut de Recherches en Informatique de Nantes, Université de Nantes, Nantes Cedex 03, France

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  • This is the only up-to-date survey of specification techniques

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (15 chapters)

  1. Front Matter

    Pages I-XXIII
    Download chapter PDF

  2. State-Based Approaches

    1. Front Matter

      Pages 1-1
      Download chapter 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
      Download chapter 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
      Download chapter 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
    Download chapter PDF
Back to top

Keywords

About this book

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.

Editors and Affiliations

  • 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

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation