Modélisation et analyse de systèmes asynchrones avec CADP

Radu Mateescu 1
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Résumé : La conception des systèmes industriels critiques comportant du parallélisme asynchrone nécessite l'utilisation de méthodes formelles, assistées par des outils de vérification adaptés, afin de détecter et corriger les erreurs le plus tôt possible. Dans ce rapport, nous illustrons l'emploi de la boîte à outils CADP pour la modélisation et la vérification formelle de tels systèmes, à travers l'exemple d'une unité dédiée au perçage des pièces métalliques. Nous décrivons en langage LOTOS deux versions différentes de l'unité, régies par un contrôleur principal séquentiel, respectivement parallèle. Ensuite, nous effectuons la génération et la minimisation des deux espaces d'états sous-jacents, ainsi que l'inspection visuelle de celui, plus petit, correspondant à la version équipée du contrôleur séquentiel. Finalement, nous analysons le comportement des deux versions de l'unité de perçage en employant deux méthodes de vérification complémentaires, basées sur les bisimulations (equivalence checking) et les logiques temporelles (model checking).
Type de document :
Rapport
[Rapport de recherche] RR-5953, INRIA. 2006, pp.31
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00088076
Contributeur : Rapport de Recherche Inria <>
Soumis le : mardi 1 août 2006 - 11:34:55
Dernière modification le : jeudi 11 janvier 2018 - 06:22:03
Document(s) archivé(s) le : lundi 20 septembre 2010 - 16:38:27

Fichiers

Identifiants

  • HAL Id : inria-00088076, version 2

Collections

Citation

Radu Mateescu. Modélisation et analyse de systèmes asynchrones avec CADP. [Rapport de recherche] RR-5953, INRIA. 2006, pp.31. 〈inria-00088076v2〉

Partager

Métriques

Consultations de la notice

200

Téléchargements de fichiers

152