Abstract FR:

Nous proposons dans notre thèse une nouvelle méthodologie pour le développement des protocoles de communication et des applications réparties en explorant une approche de synthèse automatisée. Apres avoir effectué un état de l'art sur les techniques de synthèse de protocoles, nous présentons, dans la première partie de la thèse, une nouvelle méthode de synthèse de spécifications de protocoles à partir de spécifications de services dans un modèle de réseaux de Petri interprétés. Notre approche est basée sur un nouveau concept de raffinement de réseaux de Petri qui assure la correction des protocoles construits de façon incrémentale. L'intérêt principal de cette méthode par rapport aux techniques analytiques est qu'elle évite la phase supplémentaire de validation du protocole qui passe souvent par une analyse exhaustive dont le problème fondamental est l'explosion combinatoire. De plus, le coût de construction des protocoles est considérablement diminué. Partant d’une description de service, notre technique de synthèse permet de dériver automatiquement au niveau protocole l’ensemble des fonctionnalités suivantes : (1) traitements répartis, (2) flot de contrôle, (3) flot de données, (4) contrôle de la cohérence des données,(5) et choix distribué. Elle constitue, de ce fait, un « bon » compromis entre le pouvoir de synthèse et le pouvoir d’expression des services relativement aux techniques existantes. Dans la deuxième partie de la thèse nous présentons une application réelle de notre méthode de synthèse à la conception du protocole de transport ISO de base (ISO 8073), le point de départ de la conception étant la spécification du service de transport ISO 8072. Dans la troisième partie de la thèse, nous présentons un ensemble d'outils logiciels pour la synthèse automatique de protocoles que nous appelons STEPS (Software Toolset for automatEd Protocol Synthesis). Nous avons développé cet ensemble d'outils afin de démontrer l'utilité et la faisabilité de l'approche de synthèse que nous proposons. Lla sémantique de notre modèle de spécification étant assez proche de celle du langage Estelle, nous proposons une extension de notre démarche pour la synthèse de spécifications de protocoles dans le langage Estelle. L'intérêt est que ces spécifications peuvent être directement exploitées par des outils existants afin de générer automatiquement du code exécutable ou d’effectuer des simulations et des évaluations de performance.