VERNIER Isabelle
Direction de recherche : Serge HADDAD
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
Publications 1994-2020
-
2020
- M. Jaume, M. Journault, M.‑J. Lesot, P. Manoury, I. Mounier : “Logique pour l’informatique”, (Ellipses), (ISBN: 9782340042612) (2020)
-
2014
- A. Yessad, I. Mounier, J.‑M. Labat, F. Kordon, Th. Carron : “Have you found the error? A Formal Framework for Learning Game Verification”, 9th European Conference on Technology Enhanced Learning, vol. 8719, Lecture Notes in Computer Science, Graz, Austria, pp. 476-481, (Springer) (2014)
- A. Yessad, I. Mounier, Th. Carron, F. Kordon, J.‑M. Labat : “Formal Framework to improve the reliability of concurrent and collaborative learning games”, EAI Endorsed Transactions on Serious Games, vol. 14 (2), pp. e4, (ICST) (2014)
-
2013
- 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)
-
2011
- S. Baarir, C. Braunstein, E. Encrenaz, J.‑M. Ilié, I. Mounier, D. Poitrenaud, S. Younes : “Feasibility Analysis for Robustness Quantification by Symbolic Model Checking”, Formal Methods in System Design, vol. 39 (2), pp. 165-184, (Springer Verlag) (2011)
- 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)
-
2008
- X. Blanc, I. Mounier, A. Mougenot, T. Mens : “Detecting Model Inconsistency Through Operation-Based Model Construction”, 30th International Conference on Software Engineering (ICSE 2008), Leipzig, Germany, pp. 511-520, (ACM) (2008)
-
2006
- X. Blanc, I. Mounier : “UML2 pour les développeurs”, 202 pages, (Eyrolles), (ISBN: 221212029X) (2006)
-
2004
- 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)
- I. Vernier, E. Paviot‑Adet : “Modélisation et vérification de l’interopérabilité de services de télécommunication”, chapitre de Vérification et mise en oeuvre de réseaux de Petri, pp. 233-252, (Hermes Science), (ISBN: 2-7462-0445-2) (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)
- F. Kordon, I. Vernier‑Mounier, E. Paviot‑Adet, D. Regep : “Formal Verification of Embedded Distributed Systems in a Prototyping Approach”, International Workshop on Engineering Automation for Software Intensive System Integration, Monterey, United States (2001)
- M. Doche, I. Vernier‑Mounier, F. Kordon : “Modular Approach to Specify and Validate an Electrical Fligh Control System”, Formal Method Europe (FME '2001), vol. 2021, Lecture Notes in Computer Science, Berlin, Germany, pp. 590-610, (Springer-Verlag) (2001)
-
1997
- I. Vernier : “Model Checking and Parameterized Distributed Systems”, (1997)
-
1994
- I. Vernier : “Graphe symbolique paramétré de réseaux de Petri et Logique temporelle”, thèse, soutenance 06/12/1994, direction de recherche Haddad, Serge (1994)