Graphe symbolique paramétré de réseaux de Petri et Logique temporelle

Isabelle VERNIER

IBP-Masi 1994/Th08: THÈSE de DOCTORAT de l'UNIVERSITÉ PARIS 6 Masi / Masi research reports
258 pages - Février/February 1995 - French document.

PostScript : 5207 Ko /Kb

Titre / Title: Graphe symbolique paramétré de réseaux de Petri et Logique temporelle

Résumé : Les programmes parallèles sont souvent définis pour un nombre fini mais non déterminé de processus. On peut alors souhaiter vérifier des propriétés des programmes quel que soit le nombre de processus. Le programme défini pour un nombre fixé de processus est un programme instancié. Il a été prouvé que dans le cas général la vérification paramétrée, i.e. sans fixer le nombre de processus, est un problème indécidable. Cependant, de nombreux travaux ont eu pour but de résoudre ce problème pour des cas particuliers. Les méthodes proposées sont non programmables, semi-décidables, avec des cas d'échec ou imposent des restrictions importantes sur les propriétés et les modèles étudiés.
Nous proposons une méthode de vérification paramétrée de programmes parallèles en utilisant une approche nouvelle. Nous représentons de manière symbolique, par un graphe, l'ensemble des évolutions possibles de presque tous les programmes instanciés. Le "presque tous" est dû au fait que le graphe symbolique n'est représentatif des états accessibles d'un programme instancié que si le nombre de processus est supérieur à une borne calculée lors de la construction du graphe. Le graphe symbolique peut être utilisé comme structure de vérification de propriétés. La méthode de vérification paramétrée que nous proposons présente des cas d'échec qui sont détectés par les algorithmes la mettant en oeuvre. Ces cas d'échec sont cohérents avec le fait que le problème que nous souhaitons résoudre est indécidable dans le cas général. Nous avons prouvé que lorsqu'aucun cas d'échec n'est rencontré les algorithmes se terminent en temps fini, le graphe construit représente bien l'ensemble de comportements souhaité et le résultat de la vérification est correct. Nous représentons les programmes par des réseaux de Petri et les propriétés par des formules de logique temporelle de temps arborescent.

Abstract : Parallel programs usually involve a finite but unknown number of processes. Therefore, it seems to be necessary to verify properties of such programs regardless of the number of processes. A program with a fixed number of processes is an instanciated program. The parameterized verification, i.e., without fixing the number of processes, is in general an undecidable problem. However, some researchers have proposed solutions for particular cases. The proposed methods are not programmable, semi-decidable, fail sometimes or set strong conditions on the properties or studied programs.
We propose a new approach to solve part of the parameterized verification problem. We represent by a symbolic graph the set of the executions of almost all the instanciated programs. The restriction "almost all" is due to the fact that the symbolic graph represents the accessible states of an instanciated program only if the number of processes is greater than a bound. This minimal bound is computed while the graph is built. The symbolic graph can be used as the structure needed for the verification of properties. The parameterized verification method we propose can have failure cases that are detected by the algorithms that implement the method. These failure cases are consistent with the fact that the problem we partially solve is in general undecidable. We have proved that when there is no failure, the algorithms run in a finite time, the symbolic graph represents the expected set of behaviors and the verification result is correct. The programs are represented by Petri nets and the properties by branching time temporal logic formulas.

Publications internes Masi 1994 / Masi research reports 1994