Techniques de vérification basées sur des représentations symboliques par automates et l'abstraction guidée par les contre-exemples
Institution:
Paris 7Disciplines:
Directors:
Abstract EN:
This thesis studies automatic verification techniques where programs are represented symbolically by automata. The set of configurations of such programs are represented by automata whereas instructions are represented by transducers. Computing the set of reachable states of such programs is an important ingredient for the verification of safety properties. This problem is undecidable, since the naive iterative computation does not terminate in general. Therefore, one has to use techniques to accelerate the computation. One of the techniques mainly studied consists to over-approximate the set of reachable states to enforce the convergence of the computation. These over-approximation techniques can introduce behaviours that do not exist in the program and for which the property i false. In that case, we check if the counterexamples is present in real program or due to the upper approximation. In the latter case, we use refinement techniques in order to eliminate the spurious counterexample from our abstraction and restart the computation. Using this abstract-check-refine loop, we propose techniques in order to verify sequential, non-recursive programs manipulating linked lists. We develop methods allowing to represent memory configurations as automata, and instructions as transducers. We then propose specific abstraction and refinement techniques for such representations. Then, we show that this kind of programs can also be represented like counter automata, i. E. , only few special cells of the heap (and their number is finite) are relevant and counters indicating the number of elements between this points allows to represent the heap of the program. We develop then methods for counter automata verification using the abstract-check-refine loop for this special kind of automata. We have tested our methods with a tool that supports the automaton described previously. In an other part of the thesis, we study the size of the counterexamples for Buchi automaton that represent the product between a linear temporal logic formula and a finite automaton. These counterexamples allow to correct the program and it is important to have as small as possible counterexamples to improve the time needed for the correction. Using SPIN's memory representation for a state, such algorithms have to optimize memory usage while keeping time complexity as small as possible.
Abstract FR:
Cette thèse étudie les techniques de vérification automatiques de propriétés d'accessibilité pour des programmes représentées symboliquement par des automates. Les ensembles de configurations des programmes sont représentés par des automates tandis que les instructions sont représentées par des transducteurs. Calculer l'ensemble des états accessibles est à la base de la vérification de propriétés de sûreté. C'est un problème indécidable, le calcul itératif naïf ne termine pas en général. Il faut alors utiliser des techniques permettant d'accélérer ce calcul. Une des techniques principalement étudiée consiste à sur-approximer les ensembles accessibles afin de forcer la convergence du calcul. Ces sur-approximations peuvent induire des comportements n'existant pas dans le programme réel pour lesquelles la propriété à vérifier serait fausse. Dans ce cas, nous testons, si les contre-exemples appartiennent au programme réel, et dans le cas où ces contre-exemples ne seraient dus qu'à la sur-approximation, nous automatisons des raffinements des abstractions. Partant de cette méthodologie, nous proposons des techniques afin de vérifier les programmes séquentiel, sans récursion, mais manipulant des listes chaînées. Nous développons alors des techniques permettant dans un premier temps d'exprimer les configurations mémoires de tels programmes sous forme d'automates, et les instructions sous formes de transducteurs. Nous développons ensuite des des techniques de sur-approximation adaptées à ce type particulier d'automates. Nous montrons ensuite que de tels programmes peuvent être vus comme des automates à compteurs, i. E. , que seuls quelques points des tas mémoires (qui sont en nombre finis) sont relevant et que des compteurs indiquant le nombre d'éléments entre ces points permettent de donner une représentation du comportement du programme. Nous développons ensuite des techniques de vérification d'automates à compteurs, en utilisant des techniques d'abstraction-vérificaiton-raffinement pour ce type d'automates. Nous avons développé un outil permettant la vérification de tels programmes. Dans un second temps, nous étudions le problème de la taille des contre-exemples sur des automates de Bùchi représentant le produitentre une formule de logique temporelle linéaire et un automate fini. Les contre-exemples permettent la correction des programmes, et il est important de pouvoir travailler sur des contre-exemples les plus petits possibles. De tels algorithmes nécessitent de d'optimiser l'espace mémoire utilisé pour le stockage des éléments tout en essayant de garder une complexité en temps acceptable.