责任导师 : 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.

2011-2014 刊物