LIP6 1997/011

• Rapports de recherche
  "Model Checking" et Systèmes Répartis Paramétrés
• I. Vernier
• 17 pages - 26/07/1997- document en - http://www.lip6.fr/lip6/reports/1997/lip6.1997.011.ps.gz - 344 Ko
• Contact : Isabelle.Vernier (at) nulllip6.fr
• Ancien Thème : SRC
Nous proposons une solution partielle à la vérification de propriétés d'un ensemble de programmes instances d'un même algorithme. Le paramètre instancié est le nombre de processus. Tous les programmes possibles doivent satisfaire un même ensemble de propriétés. Les algorithmes sont modélisés par des réseaux de Petri avec gardes. L'originalité de notre travail est de construire un graphe symbolique permettant de vérifier des formules de logique temporelle. Ces propriétés peuvent concernerle comportement global des programmes ou un seul processus. Les noeuds du graphe symbolique sont des prédicats représentant des ensembles d'états.
• Mots clés : Vérification, validation, logique temporelle, systèmes paramétrés, réseaux de Petri
• Directeur de la publication : Denis.Poitrenaud (at) nulllip6.fr