Supervision : Fabrice KORDON

Co-supervision : DURET-LUTZ Alexandre

Improving the Model Checking of Stutter-Invariant LTL Properties

Software systems have become ubiquitous in our everyday life. They replace humans for critical tasks that involve high costs and even human lives. The serious consequences caused by the failure of such systems make crucial the use of rigorous methods for system validation. One of the widely-used formal verification methods is the automata-theoretic approach to model checking. It takes as input a model of the system and a property, and answers if the model satisfies or not the property. To achieve this goal, it translates the negation of the property in an automaton and checks whether the product of the model and this automaton is empty. Although it is automatic, this approach suffers from the combinatorial explosion of the resulting product. To tackle this problem, especially when checking stutter-invariant LTL properties, we firstly improve the two-pass verification algorithm of Testing automata (TA), then we propose a transformation of TA into a normal form (STA) that only requires a single-pass verification algorithm. We also propose a new type of automata: the TGTA. These automata also enable a check in a single-pass and without adding artificial states; it combines the benefits of TA and generalized Büchi automata (TGBA). TGTA improve the explicit and symbolic model-checking approaches. In particular, by combining TGTA with the saturation technique, the performances of the symbolic approach has been improved by an order of magnitude compared to TGBA. Used in hybrid approaches TGTA prove complementary to TGBA.
All the contributions of this work have been implemented in SPOT and LTS-ITS, respectively, an explicit and a symbolic open source model-checking libraries.

2011-2014 Publications

• 2014
  • A. Ben Salem : “Model checking adapté aux spécifications et propriétés à vérifier”, thesis, phd defence 09/25/2014, supervision Kordon, Fabrice, co-supervision : Duret-lutz, Alexandre (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)
• 2012
  • A. Ben Salem, A. Duret‑Lutz, F. Kordon : “Model Checking using Generalized Testing Automata”, LNCS Transactions on Petri Nets and Other Models of Concurrency, vol. 7400 (VI), pp. 94-122, (Springer) (2012)
• 2011
  • A. Ben Salem, A. Duret‑Lutz, F. Kordon : “{Generalized Büchi Automata versus Testing Automata for Model Checking}”, 2^nd workshop on Scalable and Usable Model Checking for Petri Nets and other models of Concurrency (SUMo 2011), vol. 726, CEUR-WS, Newcastle, United Kingdom, pp. 65-79, (CEUR) (2011)