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.


Model Check Transition System Temporal Logic Transition Relation Linear Temporal Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


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