Supervision : Fabrice KORDON

Co-supervision : ILIÉ Jean-Michel

Techniques for Model-checking of high-level specifications

The increasing complexity of distributed applications makes their dependability a problematic issue. Model-checking is a formal method for automatically validating a system, based on an exhaustive exploration of its behaviors, but that is challenged by the combinatorial state-space explosion problem. To address this problem, we propose an approach based on automatic symmetry analysis of models and of properties expressed in Linear Temporal Logic (LTL), allowing construction of a quotient state graph that supports verification. We combine this approach with symbolic representations, thus offering an extremely compact storage solution. We define a flexible hierarchical decision diagram model, that allows to efficiently exploit a compositional description of a system. Finally, we place our techniques within a model-based rapid application development methodology, to allow their use in an industrial context.

Four past PhD students (2009 - 2013) at Sorbonne University

2002-2024 Publications

• 2024
  • N. Amat, E. Amparore, B. Berthomieu, P. Bouvier, S. Zilio, F. Hulin‑Hubard, P. Jensen, L. Jezequel, F. Kordon, Sh. Li, E. Paviot‑Adet, L. Petrucci, J. Srba, Y. Thierry‑Mieg, K. Wolf : “Behind the Scene of the Model Checking Contest, Analysis of Results from 2018 to 2023”, TOOLympics Challenge 2023, vol. 14550, Lecture Notes in Computer Science, Paris, France, pp. 52-89, (Springer Nature Switzerland), (ISBN: 978-3-031-67695-6) (2024)
• 2023
  • Y. Thierry‑Mieg : “Efficient Strategies to Compute Invariants, Bounds and Stable Places of Petri nets”, PNSE’23: Petri Nets for Software Engineering,, Lisbon, Portugal (2023)
• 2022
  • E. Paviot‑Adet, D. Poitrenaud, E. Renault, Y. Thierry‑Mieg : “LTL under reductions with weaker conditions than stutter-invariance”, Lecture Notes in Computer Science (LNCS), vol. 13273, Formal Techniques for Distributed Objects, Components, and Systems, Lucca, Italy, pp. 170–187, (Springer Cham), (ISBN: 978-3-031-08679-3) (2022)
  • Y. Thierry‑Mieg : “Symbolic and Structural Model-Checking”, Fundamenta Informaticae, vol. 183 (3-4), pp. 319–342, (IOS Press) (2022)
• 2020
  • Y. Thierry‑Mieg : “Structural Reductions Revisited”, 41ST INTERNATIONAL CONFERENCE ON APPLICATION AND THEORY OF PETRI NETS AND CONCURRENCY, Paris, France (2020)
• 2019
  • F. Kordon, M. Leuschel, J. Van De Pol, Y. Thierry‑Mieg : “Software Architecture of Modern Model Checkers”, chapter in Computing and Software Science, State of the Art and Perspectives, vol. 10000, Lecture Notes in Computer Science, pp. 393-419, (Springer) (2019)
  • S. Pinchinat, B. Fila, F. Wacheux, Y. Thierry‑Mieg : “Attack Trees: A Notion of Missing Attacks”, GraMSec 2019 - 6^th International Workshop on Graphical Models for Security, vol. 11720, Lecture Notes in Computer Science, Hoboken, NJ, United States, pp. 23-49 (2019)
  • E. Amparore, B. Berthomieu, G. Ciardo, S. Dal Zilio, F. Gallà, L. Hillah, F. Hulin‑Hubard, P. Jensen, L. Jezequel, F. Kordon, D. Le Botlan, T. Liebke, J. Meijer, A. Miner, E. Paviot‑Adet, J. Srba, Y. Thierry‑Mieg, T. Van Dijk, K. Wolf : “Presentation of the 9^th Edition of the Model Checking Contest”, Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Proceedings, Part III, vol. 11429, Prague, Czechia, pp. 50-68 (2019)
• 2018
  • F. Kordon, H. Garavel, L. Hillah, E. Paviot‑Adet, L. Jezequel, F. Hulin‑Hubard, E. Amparore, M. Beccuti, B. Berthomieu, H. Evrard, P. Jensen, D. Le Botlan, T. Liebke, J. Meijer, J. Srba, Y. Thierry‑Mieg, J. Van De Pol, K. Wolf : “MCC’2017 - The Seventh Model Checking Contest”, LNCS Transactions on Petri Nets and Other Models of Concurrency, vol. 11090, Lecture Notes in Computer Science, pp. 181-209, (Springer) (2018)
  • F. Kordon, Y. Thierry‑Mieg : “Self-adaptive Model Checking, the Next Step?”, Application and Theory of Petri Nets and Concurrency, Bratislava, Slovakia (2018)
  • Quentin L. Meunier, Y. Thierry Mieg, E. Encrenaz : “Modeling a Cache Coherence Protocol with the Guarded Action Language”, Workshop on Models for Formal Analysis of Real Systems, Thessaloniki, Greece (2018)
• 2016
  • Y. Thierry‑Mieg : “From Symbolic Verification to Domain Specific Languages”, habilitation, phd defence 12/07/2016 (2016)
  • B. Bérard, P. Lafourcade, L. Millet, M. Potop‑Butucaru, Y. Thierry‑Mieg, S. Tixeuil : “Formal verification of mobile robot protocols”, Distributed Computing, vol. 29 (6), pp. 459-487, (Springer Verlag) (2016)
  • Y. Thierry‑Mieg : “Bridging the Gap Between Formal Methods and Software Engineering Using Model-based Technology”, Petri Nets and Software Engineering. International Workshop, PNSE'16, Proceedings, Torun, Poland (2016)
• 2015
  • Y. Thierry Mieg : “Symbolic Model-Checking using ITS-tools”, Tools and Algorithms for the Construction and Analysis of Systems, vol. 9035, Lecture Notes in Computer Science, London, United Kingdom, pp. 231-237, (Springer Berlin Heidelberg) (2015)
• 2014
  • Y. Zhang, B. Bérard, L. Hillah, F. Kordon, Y. Thierry‑Mieg : “Controllability for Discrete Event Systems Modeled in VeriJ”, International Journal of Critical Computer-Based Systems, vol. 5 (3/4), pp. 218-240, (Inderscience) (2014)
  • A. Ben Salem, A. Duret‑Lutz, F. Kordon, Y. Thierry‑Mieg : “Symbolic Model Checking of stutter invariant properties Using Generalized Testing Automata”, 20^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2014, vol. 8413, Lecture Notes in Computer Science, Grenoble, France, pp. 440-454, (Springer) (2014)
• 2013
  • Y. Ben Maïssa, F. Kordon, S. Mouline, Y. Thierry‑Mieg : “Modeling and Analyzing Wireless Sensor Networks with VeriSensor: an Integrated Workflow”, LNCS Transactions on Petri Nets and Other Models of Concurrency, vol. VIII, pp. 24-47, (Springer) (2013)
  • Y. Zhang, B. Bérard, L. Hillah, Y. Thierry‑Mieg : “Semi-Automatic Controller Design of Java-like Models”, Workshop on Formal Techniques for Java-like Programs, FTfJP 2013, Montpellier, France, pp. 3:1-3:7, (ACM) (2013)
  • M. Colange, S. Baarir, F. Kordon, Y. Thierry‑Mieg : “Towards Distributed Software Model-Checking using Decision Diagrams”, 25^th International Conference on Computer Aided Verification (CAV), vol. 8044, Lecture Notes in Computer Science, Saint-Petersbourg, Russian Federation, pp. 830-845, (Springer Verlag) (2013)
  • B. Bérard, L. Millet, M. Gradinariu Potop‑Butucaru, Y. Thierry‑Mieg, S. Tixeuil : “Vérification formelle et robots mobiles”, 15^es Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications (AlgoTel), Pornic, France, pp. 1-4, (Nisse, Nicolas et Rousseau, Franck et Busnel, Yann) (2013)
  • B. Bérard, L. Millet, M. Potop‑Butucaru, Y. Thierry‑Mieg, S. Tixeuil : “Formal verification of Mobile Robot Protocols”, (2013)
  • F. Kordon, A. Linard, M. Becutti, D. Buchs, L. Fronc, L. Hillah, F. Hulin‑Hubard, F. Legond‑Aubry, N. Lohmann, A. Marechal, E. Paviot‑Adet, F. Pommereau, C. Rodríguez, Ch. Rohr, Y. Thierry‑Mieg, H. Wimmel, C. Wolf : “Web Report on the Model Checking Contest @ Petri Net 2013”, (2013)
• 2012
  • F. Kordon, B. Bérard, Y. Thierry‑Mieg, Y. Ben Maïssa : “Hierarchy is Good For Discrete Time: a Compositional Approach to Discrete Time Verification”, Dagstuhl seminar "Architecture-Driven Semantic Analysis of Embedded Systems", Dagstuhl, Germany, pp. 38-39 (2012)
  • M. Colange, F. Kordon, Y. Thierry‑Mieg, S. Baarir : “State Space Analysis using Symmetries on Decision Diagrams”, 12^th International Conference on Application of Concurrency to System Design (ACSD'2012), Hamburg, Germany, pp. 164-172, (IEEE Computer Society) (2012)
  • Y. Ben Maïssa, F. Kordon, S. Mouline, Y. Thierry‑Mieg : “Modeling and Analyzing Wireless Sensor Networks with VeriSensor”, Petri Net and Software Engineering (PNSE), vol. 851, CEUR Workshop Proceedings, Hamburg, Germany, pp. 60-76 (2012)
  • F. Kordon, A. Linard, D. Buchs, M. Colange, S. Evangelista, K. Lampka, N. Lohmann, E. Paviot‑Adet, Y. Thierry‑Mieg, H. Wimmel : “Report on the Model Checking Contest at Petri Nets 2011”, LNCS Transactions on Petri Nets and Other Models of Concurrency, vol. 7400 (VI), Lecture Notes in Computer Science, pp. 169-196, (Springer) (2012)
• 2011
  • A. Duret‑Lutz, K. Klai, D. Poitrenaud, Y. Thierry‑Mieg : “Self-Loop Aggregation Product - A New Hybrid Approach to On-the-Fly LTL Model Checking”, 9^th International Symposium on Automated Technology for Verification and Analysis (ATVA'11), vol. 6996, Lecture Notes in Computer Science, Taipei, Taiwan, Province of China, pp. 336-350, (Springer) (2011)
  • Y. Zhang, B. Bérard, L. Hillah, F. Kordon, Y. Thierry‑Mieg : “Modeling complex systems with VeriJ”, 5^th Verification and Evaluation of Computer and Communication System (VECOS), Tunis, Tunisia, pp. 34-45, (British Informatics Society Ltd) (2011)
  • M. Colange, S. Baarir, F. Kordon, Y. Thierry‑Mieg : “Crocodile: a Symbolic/Symbolic tool for the analysis of Symmetric Nets with Bag”, 32^nd International Conference on Petri Nets and Other Models of Concurrency (ICATPN 2011), vol. 6709, Lecture Notes in Computer Science, Newcastle, United Kingdom, pp. 338-347, (Springer) (2011)
  • Y. Thierry‑Mieg, B. Bérard, F. Kordon, D. Lime, O. Roux : “{Compositional Analysis of Discrete Time Petri nets}”, 1^st workshop on Petri Nets Compositions (CompoNet 2011), vol. 726, CEUR-WS, Newcastle, United Kingdom, pp. 17-31, (CEUR) (2011)
  • J.‑F. Pradat‑Peyre, Y. Thierry‑Mieg : “Verification of Finite-State Systems”, chapter in Models and Analysis in Distributed Systems, pp. 155-220, (Wiley), (ISBN: 9781848213142) (2011)
• 2010
  • Y. Zhang, B. Bérard, F. Kordon, Y. Thierry‑Mieg : “Automated Controllability and Synthesis with Hierarchical Set Decision Diagrams”, 11^th International Workshop on Discrete Event Systems (WODES'10), Berlin, Germany, pp. 281-286, (IFAC/Elsevier) (2010)
  • F. Kordon, Y. Thierry‑Mieg : “Experiences in Model Driven Verification of Behavior with UML”, Foundations of Computer Software, Future Trends and techniques for Development, 15^th Monterey Workshop 2008, Budapest, Revised Selected Papers, vol. 6028, Lecture Notes in Computer Science, Budapest, Hungary, pp. 181-200, (Springer) (2010)
  • B. Charroux, A. Osmani, Y. Thierry‑Mieg : “UML 2 : Pratique de la Modélisation”, Synthex Informatique, (Pearson), (ISBN: 978-2744074660) (2010)
• 2009
  • A. Hamez, Y. Thierry‑Mieg, F. Kordon : “Building Efficient Model Checkers using Hierarchical Set Decision Diagrams and Automatic Saturation”, Fundamenta Informaticae, vol. 94 (3-4), pp. 413-437, (Polskie Towarzystwo Matematyczne) (2009)
  • Y. Thierry‑Mieg, D. Poitrenaud, A. Hamez, F. Kordon : “Hierarchical Set Decision Diagrams and Regular Models”, 15^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), vol. 5505, Lecture Notes in Computer Science, York, United Kingdom, pp. 1-15, (Springer) (2009)
• 2008
  • Y. Thierry‑Mieg, L. Hillah : “UML Behavioral Consistency Checking Using Instantiable Petri nets”, Innovations in Systems and Software Engineering, vol. 4 (3), pp. 293-300, (Springer Verlag) (2008)
  • A. Hamez, Y. Thierry‑Mieg, F. Kordon : “Hierarchical Set Decision Diagrams and Automatic Saturation”, 29^th International Conference on Petri Nets and Other Models of Concurrency (ICATPN 2008), vol. 5062, Lecture Notes in Computer Science, Xian, China, pp. 211-230, (Springer-Verlag) (2008)
  • B. Bérard, S. Haddad, L. Hillah, F. Kordon, Y. Thierry‑Mieg : “Collision Avoidance in Intelligent Transport Systems: towards an Application of Control Theory”, 9^th International Workshop on Discrete Event Systems (WODES'08), Goteborg, Sweden, pp. 346-351, (IEEE Computer Society) (2008)
  • B. Charroux, A. Osmani, Y. Thierry‑Mieg : “UML 2, 2^e édition (Broché) Pratique de la Modélisation”, Collection INFORMATIQUE - SYNTHEX, 256 pages, (Pearson Education), (ISBN: 978-2744072871) (2008)
• 2007
  • A. Hamez, F. Kordon, Y. Thierry‑Mieg, F. Legond‑Aubry : “dmcG: a distributed symbolic model checker based on GreatSPN”, ICATPN'07 Proceedings of the 28^th international conference on Applications and theory of Petri nets and other models of concurrency, vol. 4546, Lecture Notes in Computer Science, Siedlce, Poland, pp. 495-504, (Springer) (2007)
  • A. Hamez, F. Kordon, Y. Thierry‑Mieg : “libDMC: a library to Operate Efficient Distributed Model Checking”, Parallel and Distributed Processing Symposium, 2007. IPDPS 2007. IEEE International, Long Beach, California, United States (2007)
• 2006
  • A. Hamez, L. Hillah, F. Kordon, A. Linard, E. Paviot‑Adet, X. Renault, Y. Thierry‑Mieg : “New Features in CPN-AMI 3 : Focusing on the Analysis of Complex Distributed Systems”, 6^th International Conference on Application of Concurrency to System Design (ACSD '06), Turku, Finland, pp. 273-275, (IEEE Computer Society) (2006)
  • F. Gilliers, F. Kordon, Y. Thierry‑Mieg : “Processus de fabrication de systèmes répartis centré sur un modèle : l’expérience du projet MORSE”, La Revue de l'électricité et de l'électronique, vol. 3, pp. 102-111, (Société de l'Électricité, de l'Électronique et des Technologies de l'Information et de la Communication) (2006)
  • Ch. Choppy, S. Haddad, H. Klaudel, F. Kordon, L. Petrucci, Y. Thierry Mieg : “Tutorial on Formal Methods for Distributed and Cooperative Systems”, 3^rd International Colloquium on Theoretical Aspects of Computing (ICTAC 2006), vol. 4281, Lecture Notes in Computer Science, Tunis, Tunisia, pp. 362-365 (2006)
  • J.‑M. Ilié, Y. Thierry‑Mieg, S. Baarir : “Vérification efficace des systèmes finis”, chapitre de Méthodes Formelles pour les Systèmes Répartis et Coopératifs, Traités IC2 - Informatique et systèmes d'information, pp. 171-211, (Hermes-Lavoisier), (ISBN: 2-7462-1447-4) (2006)
• 2005
  • J.‑M. Couvreur, Y. Thierry‑Mieg : “Hierarchical Decision Diagrams to Exploit Model Structure”, 25^th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'05), vol. 3731, Lecture Notes in Computer Science, Taipei, Taiwan, Province of China, pp. 443-457, (Springer-Verlag) (2005)
  • B. Charroux, A. Osmani, Y. Thierry‑Mieg : “UML 2, Synthèses de cours et exercices corrigés”, Collection Synthex, 300 pages, (Pearson Education), (ISBN: 2744071242) (2005)
• 2004
  • Y. Thierry‑Mieg : “Techniques for Model-checking of high-level specifications”, thesis, phd defence 12/13/2004, supervision Kordon, Fabrice, co-supervision : Ilié, Jean-Michel (2004)
  • Y. Thierry‑Mieg, J.‑M. Ilié, D. Poitrenaud : “A Symbolic Symbolic State Space Representation”, 24^th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE '04), vol. 3235, Lecture Notes in Computer Science, Madrid, Spain, pp. 276-291, (Springer-Verlag) (2004)
  • J. Hugues, Y. Thierry‑Mieg, F. Kordon, L. Pautet, S. Baarir, Th. Vergnaud : “On the Formal Verification of Middleware Behavioral Properties”, 9^th International Workshop on Formal Methods for Industrial Critical Systems (FMICS '04), Linz, Austria, pp. 139-157, (Elsevier) (2004)
  • Y. Thierry‑Mieg, S. Baarir, A. Duret‑Lutz, F. Kordon : “Nouvelles techniques de Model Checking pour la vérification de systèmes complexes”, Génie logiciel : le magazine de l'ingénierie du logiciel et des systèmes, vol. 69, pp. 17-23, (Génie industriel multimédia) (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)
  • D. Regep, Y. Thierry‑Mieg, F. Gilliers, F. Kordon : “Modélisation et vérification de systèmes répartis :une approche intégrée avec LfP”, Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), Rennes, France (2003)
• 2002
  • Y. Thierry‑Mieg : “Petri Net Generation from High-Level Specifications”, MOVEP '02 Summer School, Modelling and Verifying Parallel Processes, Nantes, France (2002)