VERNIER Isabelle

毕业博士 - MASI
离开日期 : 1994-12-6
https://lip6.fr/Isabelle.Mounier

责任导师 : Serge HADDAD

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

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.

答辩 : 1994-12-6

评委会 :

Pierre Azema [Rapporteur]
Brigitte Rozoy [Rapporteur]
Claude Girault
Irène Guessarian
Serge Haddad
Philippe Schnoebelen

离开日期 : 1994-12-6

1994-2020 刊物

Mentions légales
网站导航