Cette thèse s'intéresse à la vérification de systèmes automatisables par model-checking. La question sous-jacente autour de laquelle se construit la contribution est la recherche d'un compromis entre différents objectifs potentiellement contradictoires : la décidabilité des systèmes à vérifier, l'expressivité des formalismes de modélisation, l'efficacité de la vérification, et la certification des outils utilisés. Dans ce but, on choisit de baser la modélisation sur des réseaux de Petri annotés par des langages de programmation réels. Cela implique la semi-décidabilité de la plupart des questions puisque la responsabilité de la terminaison est remise entre les mains du modélisateur (tout comme la terminaison des programmes est de la responsabilité du programmeur). Afin d'exploiter efficacement ces annotations, on choisit ensuite une approche de compilation de modèle qui permet de générer des programmes efficaces dans le langage des annotations, qui sont alors exécutées de la manière la plus efficace. De plus, la compilation est optimisée en tirant partie des spécificités de chaque modèle et nous utilisons l'approche de model-checking explicite qui autorise cette richesse d'annotations tout en facilitant le diagnostique et en restant compatible avec la simulation (les modèles compilés peuvent servir à de la simulation efficace). Enfin, pour combattre l'explosion combinatoire, nous utilisons des techniques de réductions de symétries qui permettent de réduire les temps d'exploration et l'espace mémoire nécessaire. / This work focuses on verification of automated systems using model-checking techniques. We focus on a compromise between potentially contradictory goals: decidability of systems to be verified, expressivity of modeling formalisms, efficiency of verification, and certification of used tools. To do so, we use high level Petri nets annotated by real programming languages. This implies the semi-decidability of most of problems because termination is left to the modeler (like termination of programs is left to the programmer). To handle these models, we choose a compilation approach which produces programs in the model annotation language, this allows to execute them efficiently. Moreover, this compilation is optimizing using model peculiarities. However, this rich expressivity leads to the use of explicit model-checking which allows to have rich model annotations but also allows to easily recover errors from verification, and remains compatible with simulation (these compiled models can be used for efficient simulation). Finally, to tackle the state space explosion problem, we use reduction by symmetries techniques which allow to reduce exploration times and state spaces.
| Identifer | oai:union.ndltd.org:theses.fr/2013EVRY0034 |
| Date | 28 November 2013 |
| Creators | Fronc, Lukasz |
| Contributors | Evry-Val d'Essonne, Klaudel, Hanna, Pommereau, Franck |
| Source Sets | Dépôt national des thèses électroniques françaises |
| Language | French |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation, Text, StillImage |
Page generated in 0.0021 seconds