THÈSE D'UNIVERSITÉ :
THÈSE D'UNIVERSITÉ :
Yves-Marie Quemener
Novembre 1996
Nous nous intéressons dans ce document au problème de la vérification
formelle de propriétés des systèmes informatiques répartis. En
particulier, nous étudions ce problème dans le cas de protocoles
modélisés par un système d'automates communiquant par envoi de messages
\emph{via} des files. Un ensemble de méthodes de vérification couramment
utilisées consiste à construire l'espace d'états du système étudié,
qui constitue alors sa sémantique opérationnelle, et à l'utiliser pour
vérifier les propriétés intéressantes du système.
Le problème considéré est le suivant :
Quelles sont les possibilités de vérification lorsque l'espace d'états
à étudier est infini ?
Nous commen\c cons par présenter les résultats existant dans ce
domaine. Ceux-ci ne pouvant pas s'appliquer directement à l'etude des
systèmes d'automates communicants, nous proposons un algorithme permettant de
représenter l'espace d'états infini de certains de ces systèmes de
manière finie, grâce à une grammaire de graphes. L'intérêt de cette
représentation est qu'elle permet de décider un grand nombre des
propriétés vérifiées par l'espace d'états infini ainsi
représenté. En particulier, nous proposons un algorithme de
\emph{model-checking} du $\mu$-calcul sans alternation de point fixe pour de
tels espaces d'états infinis, cet algorithme s'appliquant à leur
représentation finie sous forme d'une grammaire de graphes. Nous présentons
finalement quelques résultats d'expérimentations réalisées avec un
prototype d'implémentation des algorithmes de représentation et de
model-checking.
PhD THESIS:Yves-Marie Quemener
October 1995
In that document, we are interested with the problem of formal verification of properties of distributed software systems. In particular, we study that problem for protocols described as systems of finite-state machines communicating by sending messages through queues. A set of verification methods often used consists of building the state space of the studied system, which then constitute its operationnal semantics, and of using that state space for verifying the properties of interest of that system. The problem we consider is the following: What are the possibilities of verification when the state space is infinite? We start by exposing the existing results in that field. As those results can not be directly applied to the study of systems of communicating finite-state machines, we propose an algorithm enabling to represent the infinite state space of some of those systems in a finite way, by using a graph grammar. The interest of that representation is that it enables to decide a lot of the properties satisfied by the infinite state space represented in that way. In particular, we propose an algorithm of model-checking of the $\mu$-calculus without alternating fixpoint for such infinite state spaces, this algoritm being applied to their finite representation as a graph grammar. We finally expose some experimental results obtained with a prototype of implementation of the algorithms of representation and of model-checking.