Abstract FR:

Cette these est consacree a la conception d'un outil de verification pour lotos. Lotos (language of temporal ordering specification) est un langage de specification formel normalise par l'iso en 1988. Les proprietes a verifier sur les specifications sont exprimees comme des formules d'une logique modale similaire a la logique de hennessy-milner. L'un des grands problemes des outils de verification des systemes distribues est l'explosion combinatoire des modeles generes (systemes d'etats/transitions, graphes,) par les specifications. La these se compose de deux parties. Dans la premiere partie, nous proposons une methode permettant de verifier des proprietes sans generation de systeme d'etats/transitions. Nous avons defini un ensemble de regles de gestion d'indicateurs sur l'arbre syntaxique. Ces indicateurs fournissent l'ensemble des actions permises par une specification a tout moment. La formule a verifier guide pas a pas l'exploration de l'arbre syntaxique dans le but de voir si la propriete est vrai. Un prototype implantant cette methode a ete developpe en utilisant l'atelier de genie logiciel concerto. La deuxieme partie de cette these presente une methode de verification compositionnelle. La decision de la verification d'une propriete f par une specification s depend de la verification des composants de f (sous-formules) par les differents composants de s (sous-systemes). Le probleme de cette approche reside dans la decomposition de la formule. Notre methode le resoud en tenant compte de la structure de la specification pour deriver la structure des sous-formules