Behavioral Specifications

  • Jean-François Monin
  • Michael G. Hinchey


The table example that we used in previous chapters can be qualified as functional: looking from the outside, we can view it as a function that returns an answer when it is called. We don’t have any concerns or get distracted by its internal computation and internal workings. In contrast, we can hardly understand systems which constantly react to their environments if we don’t study the series of actions they perform. This is the case for communication protocols, operating systems or command-and-control equipment. For protocols for instance, we have to consider synchronization, to prevent deadlocks, undesired arrival of messages, etc. The complexity of such protocols is by and large, concentrated in these aspects.


Paral Prefix Suffix 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag London 2003

Authors and Affiliations

  • Jean-François Monin
    • 1
  • Michael G. Hinchey
    • 2
  1. 1.France Télécom R&D, Technopole AnticipaDTL/TALLannionFrance
  2. 2.Software Verification Research CentreUniversity of QueenslandBrisbaneAustralia

Personalised recommendations