Specification and Analysis of Asynchronous Systems using CADP

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)