Abstract FR:

La verification formelle permet de garantir qu'un programme verifie un ensemble de proprietes. Pour ce faire, une methode attractive consiste a modeliser son comportement par un systeme de transition etiquetees (ste), puis a evaluer les proprietes sur ce ste par exploration exhaustive. L'interet de cette approche par model-checking est d'etre automatisable dans le cas fini, mais son inconvenient reste la taille du ste, souvent redhibitoire pour des programmes complexes. Pour palier a ce probleme, une solution possible est de considerer un ste reduit qui preserve les proprietes a verifier. Une approche naturelle consiste alors a proceder de maniere compositionelle : on genere independamment les ste associes a differentes parties du systeme global, on reduit ces ste modulo une relation appropriee, puis on compose les ste reduits ainsi obtenus. Cette technique a ete notamment mise en uvre avec succes sur des systemes de processus communiquants par rendez-vous. L'objectif de cette these est d'etendre ces resultats au cas plus difficile ou les communications ont lieu a travers des buffers asynchrones, ce qui correspond au modele d'execution de langages de specification comme sdl ou promela. Pour reduire la taille du ste obtenu lors d'une generation partielle, l'originalite de ce travail consiste alors a utiliser une notion de preordre sur les sequences d'execution du systeme : seules les sequences les plus executables conduisant a un ensemble d'etats caracteristiques de la propriete a verifier sont prises en compte. Deux types de proprietes sont notamment envisagees : l'absence de blocage et la preservation d'un langage observable. Cette approche est formellement justifiee, et un operateur de composition parallele permettant de calculer directement des ste reduits est propose. Cet operateur a ete implemente dans un outil de generation compositionnelle et sa mise en uvre sur des etudes de cas confirme largement l'interet de cette solution.