Forschungsleitung (Direction de recherche) : Fabrice KORDON

Co-Betreuung : 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.

4 Doktoren 2009 - 2013

Publikationen 2002-2023

• 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”,