Abstract FR:

Notre incapacite a prouver formellement la correction des programmes repartis rend incontournable les outils de validation de programmes repartis. Dans cette these, nous etudions le probleme de la detection de proprietes instables, les proprietes stables n'etant que de peu d'interet dans le contexte de la mise au point des programmes repartis. Nous definissons d'abord un cadre formel pour la specification et la detection de proprietes d'une execution repartie. Duquel cadre, nous nous servons pour construire et implementer des algorithmes de detection de proprietes comportementales sur les flots de controle. Il s'agit d'une instanciation du probleme de la reconnaissance d'un langage sur un graphe dirige acyclique etiquete. Nous montrons comment instancier notre algorithme generique afin de detecter des proprietes comportementales sur l'ensemble des flots de controle du graphe des etats locaux. Aussi, nous avons defini une logique qui permet de specifier et de detecter une large classe de proprietes comportementales. Une implementation des algorithmes elabores a ete realisee au sein du prototype de devermineur erebus et une etude comparative des resultats obtenus est donnee. Enfin, nous montrons comment specifier des proprietes comportementales sur l'ensemble des sequences d'etats globaux. Les comportements specifies et detectes sont alors les plus larges possibles mais ont un cout important. Nous etudions alors comment detecter des proprietes a moindre cout et notamment comment detecter des etats globaux qui soient atteints quelle que soit l'observation qu'il est possible de construire