Découpe de programmes concurrents en vue de leur vérification
Institution:
Paris, CNAMDisciplines:
Directors:
Abstract EN:
To analyse concurrent programs by using a formal model from which the whole states space is generated requires to deal with the combinatory explosion of the states space size. Quasar is an automatic tool which aims to do it at different level of its analysis process. First the program is reduced by preserving only the elements related to the studied property, then the progam is translated into a formal model (Petri net) and then analyzed by model-checking. This thesis first gives an overview of existing program slicing technics, the program reduction technic used by Quasar. Then a new approach for concurrent program slicing and the tool performing it are presented. The last part of the thesis presents the techniques used to translate a program, reduced or not, into Petri net.
Abstract FR:
Analyser des programmes concurrents en utilisant un modèle formel à partir duquel on génère l'ensemble des états accessibles par le modèle nécessite de faire face à l'explosion combinatoire du nombre de ces états. Quasar est un outil de vérification de programmes concurrents combattant ce problème à plusieurs niveaux. Tout d'abord, le programme est réduit pour ne conserver que les éléments relatifs à la propriété étudiée, puis le programme est traduit en un modèle formel (réseau de Petri) qui est ensuite analysé par une technique d'exploration exhaustive. Cette thèse présente tout d'abord un état de la découpe de programmes puis une nouvelle approche de la découpe de programmes concurrents, dite à la volée, plus adaptée à une intégration dans le processus suivi par Quasar. L'outil Yasnost, réalisé lors de cette thèse et la mettant en oeuvre est également présenté. Enfin la thèse présente les techniques utilisées pour traduire un programme, réduit ou non, en réseau de Petri.