Résumé:
Les systèmes contemporains complexes basés sur les interactions sont souvent
construits en réutilisant des entités de communication distribuées existantes qui
doivent se coordonner pour répondre aux exigences du client, du système et de
l’environnement. Dans cette thèse, nous abordons la conception de systèmes distribués composés d’entités (systèmes de transitions d’états) communiquantes via des
échanges de messages. Nous considérons les chorégraphies comme le modèle formel
permettant au développeur de décrire et de spécifier la coordination entre entités
comme un ensemble de conversations, c’est-à-dire toutes les séquences de messages
échangés entre les entités en communication. En procédant ainsi, la construction
des systèmes ne nécessite pas de construction des entités individuelles ni de leur
composition car ils peuvent être obtenus par la projection de la chorégraphie. La
rectitude de la conservation de tels messages échangés par chaque entité, obtenus
par projection, est une problématique majeure, connue sous le nom de problème
de réalisabilité. Il est impératif de vérifier la réalisabilité de la chorégraphie pour
créer des applications tierces sans erreur de coordination, par exemple, l’absence
d’interblocages, la perte et le désordre des messages, etc. Dans nos travaux [18–20],
nous avons proposé un ensemble d’opérateurs de composition permettant aux concepteurs de construire des chorégraphies réalisables décrites sous forme de protocole de
conversation. La réalisabilité est garantie par construction. Nous nous appuyons sur
la méthode B-événementiel, correcte-par-construction, pour prouver que chaque protocole de conversation construit avec nos opérateurs est réalisable. Notre approche
s’applique et évolue à un ensemble de cas d’utilisation empruntés à la littérature
et utilisés par la communauté des chercheurs. Notre approche permet également de
détecter les défaillances et que la récupération après défaillance n’est pas réalisable.
