Abstract FR:

L'apparition des defaillances dans un systeme reparti a motive la recherche de modalites automatiques afin de concevoir des algorithmes capables de les surmonter. L'auto-stabilisation tolere les defaillances transitoares en considerant que tous les processeurs reagissent d'une maniere correcte mais l'ensemble du systeme (la configuration) peut etre corrompu. Notre memoire developpe les trois axes de recherche concernant les algorithmes auto-stabilisants, plus particulierement : la conception, la verification et le raffinement. Afin de pouvoir verifier les proprietes d'un systeme reparti auto-stabilisants nous avons construit le modele, plus precisement le cadre de preuve, utilise tout au long de notre memoire. Apres avoir definie d'une maniere coherente et unitaire l'auto-stabilisation probabiliste nous avons continuer notre memoire en etudiant les diverses techniques de verification d'algorithmes auto-stabilisants. De plus, nous avons propose une nouvelle methode de composition d'algorithmes, qui par rapport aux methodes classiques renforce les algorithmes auto-stabilisants face au comportement asynchrone du systeme. Dans une composition croisee le choix du module fort (de la plateforme de transformation) est la tache la plus difficile a cause des proprietes speciales qu'un tel module doit verifier. Nous avons montre par la suite qu'il existe des algorithmes qui peuvent etre utilises en tant que plateforme de transformations dans une composition croisee. Ainsi, nous avons presente dans le quatrieme chapitre un algorithme qui est de plus solution pour le probleme de l'exclusion mutuelle locale. La derniere partie de notre memoire est une application pour les resultats theoriques obtenues auparavant. Afin de montrer que les methodes de verification et transformation presentees auparavant sont applicables aux algorithmes reels, dans le dernier chapitre nous avons etudie les plus importants problemes de l'algorithmique repartie, plus precisement ceux relies a l'allocation de ressources : l'exclusion mutuelle et sa generalisation la l-exclusion mutuelle ainsi que le probleme d'election de leader.