Preuves d'algorithmes auto-stabilisants
Institution:
Paris 11Disciplines:
Directors:
Abstract EN:
Proving algorithms in corruptible systems is a hard problem. Traditionally, such a proof is done by exhibiting decreasing functions in the system states. This method can not be generic because the functions depends too much on the algorithm. Moreover, it is often hard to find the function if the algorithm is complicated. We propose two new approach for simplifying and automating this proves. In chapter 4, we propose a simplification method for the proofs by composing the algorithm with a module which reduces the inherent non-determinism of the distributed systems. This method is based on a local mutual exclusion algorithm. The module make the proof easier by reducing the executions space. In chapter 5, we propose a partial automatization method for the proof. It works on linear topology (ring or chain). We define a formalism which allows to consider the system as a word and the algorithm as a rewriting system. This method is applied to literature examples. We show in the chapter 7, that this method can work with other topology and message passing, using an abstraction of the states. In chapter 6, we present the implementation of the automatization method. It is interactive software which allows to prove algorithms in an intuitive manner by automating the rewriting calculus.
Abstract FR:
La preuve d'algorithme dans les systèmes corruptibles est un problème difficile. Traditionnellement, ces preuves sont effectuées par l'exhibition de fonctions décroissantes sur les états du système. Cette méthode n'est pas satisfaisante car elle est trop dépendante de l'algorithme pour présenter la moindre généricité. De plus, il est souvent difficile de trouver cette fonction si l'algorithme est compliqué. Nous proposons deux approches nouvelles pour simplifier et automatiser en partie ces preuves. Dans le chapitre 4, nous proposons une méthode de simplification des preuves par une composition de l'algorithme original avec un module qui réduit le non déterminisme inhérent aux systèmes répartis. Cette méthode est basée sur un algorithme d'exclusion mutuelle locale. Elle permet de restreindre l'espace des exécutions, facilitant ainsi la preuve. Dans le chapitre 5, nous proposons une méthode d'automatisation partielle du processus de preuve d'un algorithme à condition que la topologie soit linéaire (anneau ou chaîne). Nous définissons un formalisme qui permet de considérer le système comme un mot et l'algorithme comme un système de réécriture. Cette méthode est appliquée à des exemples tirés de la littérature. Nous montrons dans les perspectives (chapitre 7) que cette méthode peut être abstraite dans certains cas, pour supporter des topologies quelconques et du passage de messages. Le chapitre 6 présente l'implémentation de la méthode d'automatisation des preuves. C'est un logiciel interactif qui permet d'effectuer ces preuves d'une façon intuitive en automatisant les calculs de réécriture.