Graphe symbolique paramétré de réseaux de Petri et Logique temporelle
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.
Soutenance : 06/12/1994
Membres du jury :
Pierre Azema [Rapporteur]
Brigitte Rozoy [Rapporteur]
Claude Girault
Irène Guessarian
Serge Haddad
Philippe Schnoebelen
Date de départ : 06/12/1994
Publications 1994-2020
2020
M. Jaume, M. Journault, M.‑J. Lesot, P. Manoury, I. Mounier : “Logique pour l’informatique”, (Ellipses), (ISBN: 9782340042612) (2020)
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)
C. Dutheillet, I. Mounier, N. Sznajder : “Distributed Control”, chapter in Models and Analysis in Distributed Systems, pp. 307-351, (Wiley), (ISBN: 9781848213142) (2011)
2010
S. Baarir, C. Braunstein, E. Encrenaz, J.‑M. Ilié, T. Li, I. Mounier, D. Poitrenaud, S. Younes : “Quantifying Robustness by Symbolic Model checking”, 1st Hardware Verification Workshop (CAV workshop), Edinburgh, United Kingdom, pp. 1-12 (2010)
2009
X. Blanc, A. Mougenot, I. Mounier, T. Mens : “Incremental Detection of Model Inconsistencies based on Model Operations”, 21st International Conference on Advanced Information Systems Engineering (CAiSE'09), vol. 5565, Lecture Notes in Computer Science, Amsterdam, Netherlands, pp. 32-46, (Springer) (2009)
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)
2003
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)
2001
G. Gaudière, A. de Groot, J. Hooman, F. Kordon, M. Lemoine, E. Paviot‑Adet, I. Vernier‑Mounier, V. Winter : “A Survey: Applying Formal Methods to a Software Intensive System”, 6th IEEE International Symposium on Hight Assurance Systems Engineering (HASE'01), Boco Raton, FL, United States, pp. 55-64, (IEEE) (2001)