Model Checking and Parameterized Distributed Systems

I. Vernier

LIP6 1997/011: Rapport de Recherche LIP6 / LIP6 research reports
17 pages - Juillet/July 1997 - Document en anglais.

PostScript : 336 Ko /Kb

Contact : par mail / e-mail

Thème/Team: Systèmes Répartis et Coopératifs

Titre français : "Model Checking" et Systèmes Répartis Paramétrés
Titre anglais : Model Checking and Parameterized Distributed Systems

Résumé : 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.

Abstract : We propose a solution to solve part of the verification problem for a set of parallel programs that are the instantiations of a same algorithm. The instantiated parameter is the number of processes. All the possible programs are supposed to satisfy the same properties. Petri nets with guarded transitions model the programs. The originality of our method is to build a symbolic graph that allows us to verify temporal properties that concern the behavior of the whole program as well as properties that concern the behavior of a single process. The nodes of the symbolic graph are predicates that represent sets of states.

Mots-clés : Vérification, validation, logique temporelle, systèmes paramétrés, réseaux de Petri

Key-words : Verification, validation, temporal logic, parameterized systems, Petri nets

Publications internes LIP6 1997 / LIP6 research reports 1997

Responsable Éditorial / Editor
webmaster@lip6.fr