LIP6 2005/008

• Rapports de recherche
  Diagrammes de Décision de Données pour l'analyse de systèmes ProMeLa
• V. Beaudenon, E. Encrenaz, S. Taktak
• 13 pages - 28/06/2005- document en - http://www.lip6.fr/lip6/reports/2005/lip6-2005-008.pdf - 355 Ko
• Contact : Vincent.Beaudenon (at) nulllip6.fr
• Ancien Thème : ASIM
Cet article montre comment vérifier des propriétés CTL sur des systèmes décrits en ProMeLa en utilisant des méthodes symboliques. On a choisi les Diagrammes de Décision de Données (DDD) comme type de données abstrait. Il s'agit d'arbres n-aires permettant de représenter des systèmes dynamiques articulant des variables entières. On décrit les principaux composant utilisés pour la vérification de systèmes ProMeLa (DDD, représentation du système ProMeLa et la transposition de ses instructions sur les DDD). Puis nous comparons notre méthode avec le Model-Checker SPIN et les techniques classiques utilisant les BDD afin de déterminer quelles sont les classes de systèmes pour lesquelles notre méthode s'avère le plus efficace.
• Mots clés : SPIN, CTL, Méthodes de Vérification Symboliques, BDDs, DDDs
• Directeur de la publication : Francois.Dromard (at) nulllip6.fr