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

Radu Mateescu

In Systèmes temps réel 1 - techniques de description et de vérification, IC2 treatise, chapter 5, pp. 151-180, Lavoisier, 2006

Full version available as INRIA Research Report RR-5953.

An English version of this chapter is available here.

Abstract:

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).

31 pages

PDF

PostScript