Preuves d'algorithmes auto-stabilisants

La preuve d'algorithme auto-stabilisants est un problème difficile. Traditionellement, 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.

Tout d'abord, 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 et la conception.

Ensuite, nous proposons une méthode d'automatisation partielle du processus de preuve d'un algorithme à condition que la topologie soit linéaire (anneau ou chaine). 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 que cette méthode peut être abstraite dans certains cas, pour supporter des topologies quelconques et du passage de messages.

Enfin, nous présentons 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.