Relatore : 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.

Pubblicazioni 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”, 9^th 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”, 7^th 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”, 1^st 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”, 21^st 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 24^th 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”, 30^th 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”, 24^th 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”, 6^th 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”, these, difesa 12/06/1994, relatore Haddad, Serge (1994)