Abstract FR:

Nous nous interessons dans ce doument au probleme de la verification formelle de proprietes des systemes informatiques repartis. En particulier, nous etudions ce probleme dans le cas de protocoles modelises par un systeme d'automates communiquant par envoi de messages via des files. Un ensemble de methodes de verification couramment utilisees conssiste a construire l'espace d'etats du systeme etudie, qui constitue alors sa semantique operationnelle, et a l'utiliser pour verifier les proprietes interessantes du systeme. Le probleme considere est le suivant: quelles sont les possibilites de verification lorsque l'espace d'etats a etudier est infini ? nous commencons par presenter les resultats existant dans ce domaine. Ceux-ci ne pouvant pas s'appliquer directement a l'etude des systemes d'automates communicants, nous proposons un algorithme permettant de representer l'espace d'etat infini de certains de ces systemes de maniere finie, grace a une grammaire de graphes. L'interet de cette representation est qu'elle permet de decider un grand nombre des proprietes verifiees par l'espace d'etats infini ainsi represente. En particulier, nous proposons un algorithme de model-checking du -calcul sans alternation de point fixe pour de tels espaces d'etats infinis, cet algorithme s'appliquant a leur representation finie sous forme d'une grammaire de graphes. Nous presentons finalement quelques resultats d'experimentations realisees avec un prototype d'implementation des algorithmes de representation et de model-checking