Skip to Main content Skip to Navigation

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

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 :
Complete list of metadata

Cited literature [89 references]  Display  Hide  Download
Contributor : Abes Star :  Contact Connect in order to contact the contributor
Submitted on : Thursday, October 19, 2017 - 10:15:41 AM
Last modification on : Monday, October 11, 2021 - 10:04:25 AM
Long-term archiving on: : Saturday, January 20, 2018 - 2:17:15 PM


Version validated by the jury (STAR)


  • HAL Id : tel-01090759, version 2


Alois 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⟩



Record views


Files downloads