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

https://hal.inria.fr/inria-00264235
Contributor : Radu Mateescu <>
Submitted on : Friday, March 14, 2008 - 4:01:41 PM
Last modification on : Thursday, November 19, 2020 - 1:00:23 PM
Long-term archiving on: : Friday, May 21, 2010 - 12:29:20 AM

File

Mateescu-08.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00264235, version 1

Collections

INRIA | CNRS | LIG | UGA

Citation

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⟩

Share

Metrics

Record views

316

Files downloads

378