Contributions à la vérification et à la validation efficaces fondées sur des modèles

Aloïs Dreyfus 1, 2
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : The thesis contributes to development of automatic methods for model-based verification and validation of computer systems. It is divided into two parts: verification and test generation. In the verification part, for the problem of regular model checking undecidable in general, two new approximation techniques are defined in order to provide efficient (semi-)algorithms. Over-approximations of the set of reachable states are computed, with the objective of ensuring the termination of the exploration of the state space. Reachable states (or over-approximations of this set of states) are represented by regular languages or, equivalently, by finite-state automata. The first technique consists in over-approximating the set of reachable states by merging states of automata, based on simple syntactic criteria, or on a combination of these criteria. The second approximation technique also merges automata states, by using transducers. For the second technique, we develop a new approach to refine approximations, inspired by the CEGAR paradigm (for Counter-Example-Guided Abstraction Refinement). These proposals have been tested on examples of mutual exclusion protocols. In the test generation part, a technique that combines the random generation with coverage criteria, from context-free models (context-free grammars, pushdown automata) is defined. Generate tests from these models (instead of doing from graphs) reduces the model abstraction level, and therefore allows having more tests executable in the real system. These proposals have been tested on the JSON grammar (JavaScript Object Notation), as well as on pushdown automata of mutually recursive functions, of an XPath query, and of the Shunting-Yard algorithm.
Document type :
Complete list of metadatas

Cited literature [89 references]  Display  Hide  Download
Contributor : Pierre-Cyrille Heam <>
Submitted on : Thursday, December 4, 2014 - 10:34:43 AM
Last modification on : Tuesday, December 18, 2018 - 4:38:25 PM
Long-term archiving on : Saturday, April 15, 2017 - 3:38:23 AM


  • HAL Id : tel-01090759, version 1



Aloïs Dreyfus. Contributions à la vérification et à la validation efficaces fondées sur des modèles. Informatique et langage [cs.CL]. Université de Franche-Comté, 2014. Français. ⟨tel-01090759v1⟩



Record views


Files downloads