Vers une évolution cohérente des chorégraphies par les méthodes formelles

Abstract

Les systèmes contemporains complexes basés sur les interactions sont souvent construits en réutilisant des entités de communications distribués existants 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) communiquant 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ées entre les entités en communication. En procédant ainsi, ne nécessite pas de construction des entités individuels ni de leur composition car ils peuvent être obtenus par la projection de la chorégraphique. La rectitude de la conservation de tels messages échangés par chaque entité, obtenus par projection, est une problématique majeur, connu 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, . . . . Dans nos traveaux [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. Tel que, 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. *********************************************************************************************************************************** Contemporary interaction-based complex systems are often built by reusing existing distributed peers which have to coordinate with each other to fulfill the client, system, and environment requirements. In this thesis, we address the design of distributed systems composed of peers (state-transitions systems) communicating through message exchanges. We consider choreographies as the formal model allowing a developer to describe and specify peers coordination as a set of conversations, i.e., all sequences of messages exchanged between the communicating peers. Proceeding this way neither require building the individual peers nor their composition as they may be obtained by the choreography projection. The correctness of the preservation of such messages exchanges by each peer obtained after projection is a key issue, known as the realizability problem. Checking choreography realizability is mandatory to build third-party applications with no coordination error, e.g., absence of deadlocks, missing messages, and erroneous messaging order. In our works [18–20], we have proposed a set of composition operators allowing designers to build realizable choreographies that are represented by conversation protocols. Realizability is guaranteed by construction. We rely on the correct-by-construction Event-B method to prove that each CP constructed using our operators is realizable. Our approach applies and scales to a set of use cases borrowed from the literature and used by the research community. Our approach allows also to detect failures and failure recovery in case realizability does not hold.