Vers une évolution cohérente des systèmes dynamiques à partir des méthodes formelles

Abstract

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.