BEN SALEM Ala Eddine

دكـتور
وحـدة : MoVe
تاريـخ المـغادرة : 31/12/2014
https://lip6.fr/Ala-Eddine.Ben-Salem

رئاسـة البـحث : Fabrice KORDON

تأطـير مـشـترك : 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.

مناقـشـة مـذكـرة : 25/09/2014

أعـضاء لجنة المناقـشة :

M. Radu Mateescu (INRIA), Rapporteur
M. Stefan Schwoon (ENS Cachan), Rapporteur
Mme. Béatrice BÉRARD (UPMC, Paris 6)
M. Didier BUCHS (Université de Genève)
M. Fabrice Kordon (UPMC, Paris 6)
M. Alexandre Duret-Lutz (EPITA)

تاريـخ المـغادرة : 31/12/2014

إصدارات 2011-2014

Mentions légales
خـريـطـة المـوقـع