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).
Type de document :
Chapitre d'ouvrage
Stephan Merz and Nicolas Navet. Modeling and Verification of Real-Time Systems - Formalisms and Software Tools, ISTE publishing / John Wiley, 2008
Liste complète des métadonnées

Littérature citée [38 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00264235
Contributeur : Radu Mateescu <>
Soumis le : vendredi 14 mars 2008 - 16:01:41
Dernière modification le : jeudi 11 janvier 2018 - 01:48:48
Document(s) archivé(s) le : vendredi 21 mai 2010 - 00:29:20

Fichier

Mateescu-08.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00264235, version 1

Collections

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〉

Partager

Métriques

Consultations de la notice

200

Téléchargements de fichiers

104