Contribution to the efficient model-based verification andtesting
Contributions à la vérification et à la validation efficaces fondées sur des modèles
Résumé
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.
Les travaux de cette thèse contribuent au développement de méthodes automatiques de vérification et de validation de systèmes informatiques, à partir de modèles. Ils sont divisés en deux parties~: vérification et génération de tests. Dans la partie vérification, pour le problème du model-checking régulier indécidable en général, deux nouvelles techniques d'approximation sont définies, dans le but de fournir des (semi-)algorithmes efficaces. Des sur-approximations de l'ensemble des états accessibles sont calculées, avec l'objectif d'assurer la terminaison de l'exploration de l'espace d'états. Les états accessibles (ou des sur-approximations de cet ensemble d'états) sont représentés par des langages réguliers, ou automates d'états finis. La première technique consiste à sur-approximer l'ensemble des états atteignables en fusionnant des états des automates, en fonction de critères syntaxiques simples, ou d'une combinaison de ces critères. La seconde technique d'approximation consiste aussi à fusionner des états des automates, mais à l'aide de transducteurs. De plus, pour cette seconde technique, nous développons une nouvelle approche pour raffiner les approximations, qui s'inspire du paradigme CEGAR. CounterExample-Guided Abstraction Refinement). Ces propositions ont été expérimentées sur des exemples de protocoles d'exclusion mutuelle. Dans la partie génération de tests, une technique qui permet de combiner la génération aléatoire avec un critère de couverture, à partir de modèles algébriques (des grammaires algébriques, des automates à pile) est définie. Générer les tests à partir de ces modèles algébriques (au lieu de le faire à partir de graphes) permet de réduire le degré d'abstraction du modèle et donc de générer moins de tests qui ne sont pas exécutables dans le système réel. Ces propositions ont été expérimentées sur la grammaire de JSON (JAvaScript Object Notation), ainsi que sur des automates à pile correspondant à des appels de fonctions mutuellement récursives, à une requête XPath, et à l'algorithme Shunting-Yard.
Loading...