**Specification and Analysis of Asynchronous Systems using CADP**

*Radu Mateescu*

In *Modeling and Verification of Real-Time Systems - Formalisms and Software Tools*, chapter 5, ISTE publishing / John Wiley, ISBN 9781848210134, 2008

A French version of this chapter is available here.

** Abstract:**

The design of complex industrial critical systems involving
asynchronous parallelism requires the use of formal methods,
assisted by appropriate verification tools, in order to detect
and correct errors as early as possible. In this chapter, we
illustrate the use of the CADP toolbox for the formal modeling
and verification of such systems by considering as an example
a unit dedicated to the drilling of metal products. We describe
in the LOTOS language two different versions of the unit,
supervised by a sequential and a parallel controller,
respectively. Then, we perform the generation and minimisation
of the two underlying state spaces, and also the inspection
(*visual checking*) of the smaller one, corresponding to the
version equipped with a sequential controller. Finally, we analyse
the behaviour of the two versions of the drilling unit by means of
two complementary verification methods, based on bisimulations
(*equivalence checking*) and temporal logics (*model
checking*).

28 pages | PostScript |