Skip to Main content Skip to Navigation
Book sections

Specification and Analysis of Asynchronous Systems using CADP

Radu Mateescu 1 
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
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).
Document type :
Book sections
Complete list of metadata

Cited literature [38 references]  Display  Hide  Download
Contributor : Radu Mateescu Connect in order to contact the contributor
Submitted on : Friday, March 14, 2008 - 4:01:41 PM
Last modification on : Wednesday, July 6, 2022 - 4:13:13 AM
Long-term archiving on: : Friday, May 21, 2010 - 12:29:20 AM


Files produced by the author(s)


  • HAL Id : inria-00264235, version 1



Radu Mateescu. Specification and Analysis of Asynchronous Systems using CADP. Stephan Merz and Nicolas Navet. Modeling and Verification of Real-Time Systems - Formalisms and Software Tools, ISTE publishing / John Wiley, 2008. ⟨inria-00264235⟩



Record views


Files downloads