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.
Defence : 12/06/1994 - 10h Jury members : Pierre Azema [Rapporteur]
Brigitte Rozoy [Rapporteur]
Th. Carron, F. Kordon, J.‑M. Labat, I. Mounier, A. Yessad : “Toward Improvement of Serious Game Reliability”, 7th European Conference on Games Based Learning, vol. 2, Porto, Portugal, pp. 80-87, (Academic Conferences and Publishing International) (2013)
S. Baarir, C. Braunstein, R. Clavel, E. Encrenaz, J.‑M. Ilié, R. Leveugle, I. Mounier, L. Pierre, D. Poitrenaud : “Complementary formal approaches for dependability analysis”, The 24th IEEE International Symposium on Defect and Fault Tolerance in VLSI Systems, Chicago, Illinois, United States, pp. 331-339, (IEEE Computer Society) (2009)
F. Bréant, J.‑M. Couvreur, F. Gilliers, F. Kordon, I. Mounier, E. Paviot‑Adet, D. Poitrenaud, D. Regep, G. Sutre : “Modeling and Verifying Behavioral Aspects”, chapter in Formal Methods for Embedded Distributed Systems - How to master the complexity, pp. 171-211, (Kluwer Academic Publishers), (ISBN: 1-4020-7996-6) (2004)
Y. Thierry‑Mieg, C. Dutheillet, I. Mounier : “Automatic Symmetry Detection in Well-Formed Nets”, 24th International Conference on Theory and Application of Petri Nets, vol. 2679, Lecture Notes in Computer Science, Eindhoven, Netherlands, pp. 82-101, (Springer) (2003)
C. Dutheillet, J.‑M. Ilié, D. Poitrenaud, I. Vernier‑Mounier : “State-Space-Based Methods and Model Checking”, chapter in Petri nets for Systems Engineering : A Guide to Modeling, Verification, and Applications, pp. 201-275, (Springer-Verlag), (ISBN: 3-540-41217-4) (2003)