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 ofcomputer 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 approxi-mation techniques are defined in order to provide efficient (semi-)algorithms. Over-approximations of the setof reachable states are computed, with the objective of ensuring the termination of the exploration of the statespace. 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 reachablestates 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 tech-nique, 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 exclusionprotocols.In the test generation part, a technique that combines the random generation with coverage criteria, fromcontext-free models (context-free grammars, pushdown automata) is defined. Generate tests from these mo-dels (instead of doing from graphs) reduces the model abstraction level, and therefore allows having moretests executable in the real system. These proposals have been tested on the JSON grammar (JavaScript ObjectNotation), as well as on pushdown automata of mutually recursive functions, of an XPath query, and of theShunting-Yard algorithm.
Document type :
Theses
Complete list of metadatas

Cited literature [89 references]  Display  Hide  Download

https://hal.inria.fr/tel-01090759
Contributor : Abes Star <>
Submitted on : Thursday, October 19, 2017 - 10:15:41 AM
Last modification on : Friday, May 17, 2019 - 11:39:12 AM
Long-term archiving on : Saturday, January 20, 2018 - 2:17:15 PM

File

these_A_DREYFUS_Alois_2014.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-01090759, version 2

Citation

Aloïs Dreyfus. Contributions à la vérification et à la validation efficaces fondées sur des modèles. Systèmes et contrôle [cs.SY]. Université de Franche-Comté, 2014. Français. ⟨NNT : 2014BESA2076⟩. ⟨tel-01090759v2⟩

Share

Metrics

Record views

169

Files downloads

220