Spécification et vérification de propriétés quantitatives sur des automates à contraintes
Institution:
Cachan, Ecole normale supérieureDisciplines:
Directors:
Abstract EN:
The ubiquity of computer systems in everyday life impose to ensure their good behavior. The use of formal verification methods allows to supply simulations that cannot be exhaustive because of the large amount of possible scenarios. Model checking is a technique to verify automatically computer systems which consists in developing algorithme to check that a specification usually expressed by some logical formula is satisfied by a model of the system. Historical specification languages use propositional variables as atomic formulas, which allows to state properties only on the control locations of the models. In this thesis, we aim at checking richer properties on the data that models can handle: counters, clocks or queues. These data have an infinite interpretation domain and so the corresponding models have an infinite amount of states. We define a general framework for the extension of temporal logics with constraints allowing to compare values of the variables at different states of an execution. We establish decidability and complexity results for model checking problems involving several instances of such extensions. We mainly use automata base techniques combining usual constructions with abstraction methods for infinite data.
Abstract FR:
L'utilisation omniprésente des systèmes informatiques impose de s'assurer de leur bon fonctionnement. Dans ce but, les méthodes de vérification formelle permettent de suppléer les simulations qui ne peuvent être complètement exhaustives du fait de la complexité croissante des systèmes. Le model checking fait partie de ces méthodes et présente l'avantage d'être complètement automatisée. Cette méthode consiste à développer des algorithmes pour vérifier qu'une spécification exprimée la plupart du temps sous la forme d'une formule logique est satisfaite par un modèle du système. Les langages historiques de spécification utilisent comme formules atomiques des variables propositionnelles qui permettent d'exprimer principalement des propriétés portant sur les états de contrôle du modèle. Le but de cette thèse est de vérifier des propriétés plus riches portant sur diverses données manipulées par les modèles: des compteurs, des horloges ou des queues. Ces données peuvent prendre une infinité de valeurs et induisent donc des modèles avec un nombre infini d'états. Nous définissons un cadre général pour l'extension des logiques temporelles avec des contraintes permettant de comparer la valeur des variables a différents états de l'exécution. Nous établissons des résultats de décidabilité et complexité pour des problèmes de model checking impliquant diverses instances de ces extensions. Nous privilégions pour cela l'approche à base d'automates en combinant des constructions connues pour les logiques propositionnelles classiques avec des méthodes d'abstraction des modèles dont les variables sont interprétées dans des domaines infinis.