Abstract FR:

La detection au plus tot des erreurs de conception d'un systeme reparti repose en particulier sur la validation des protocoles qui regissent la communication et la synchronisation. Les travaux presentes dans ce memoire portent sur la technique de description formelle estelle normalisee a l'iso et sur le prototypage d'un environnement de validation de protocoles decrits au moyen de cette technique. Deux propositions d'extensions renforcent le pouvoir d'estelle tant du point de vue de l'expression des comportements paralleles que de la description des structures de donnees echangees par des processus d'application. Un mecanisme de rendez-vous est defini de maniere formelle en s'appuyant sur les recherches anterieures pour rapprocher estelle des reseaux petri, outil de modelisation pour lequel existent des techniques de validation eprouvees. L'extension de ces techniques a des descriptions estelle est l'objet du developpement de l'outil estim qui offre a la fois des fonctionnalites de simulation pour l'analyse interactive d'un protocole et des fonctionnalites de verification pour l'obtention automatique de l'automate quotient qui caracterise le service rendu par le protocole. Les experimentations ont montre que la methodologie proposee pour l'outil estim reduit le fosse entre l'etape de validation et l'implantation reelle d'un protocole. Developpe en ml sur la base d'une semantique formelle d'estelle, le prototype realise demeure un support d'evaluation d'estelle et de ses extensions