Abstract FR:

Concevoir un algorithme distribue est un probleme difficile: il faut construire une vue globale de l'ensemble des comportements du systeme. Dans un cadre asynchrone ou chaque processus evolue a sa propre vitesse, une telle vue est quasi impossible. Par contre, si les procesus sont cadences par une horloge globale, les algorithmes deviennent alors plus faciles a construire et a comprendre. C'est a l'etude de ce modele de calcul qu'est consacre ce travail. La premiere partie etudie une classe particuliere d'algorithmes: les synchroniseurs. Ils jouent le role d'interface homogene entre les algorithmes synchrones et le reseau reel. Les synchroniseurs sont etudies d'abord d'un point de vue theorique et ensuite d'un point de vue experimentale. En particulier nous determinons quelle mise en uvre des synchroniseurs est la plus efficace. La seconde partie aborde la preuve pour assertion des algorithmes distribues synchrones. La methode consiste a profiter des points de synchronisation du modele pour connaitre un etat global du systeme. Par contre entre deux points de synchronisation, il faut se contenter d'hypotheses, notamment au niveau des receptions de messages. La correction et la completude du systeme de preuve propose sont montrees. La methode est illustree par de nombreux exemples