Abstract 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 paper, 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; ie, all sequences of messages exchanged between the communicating peers. Proceeding this way requires building neither 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, eg, absence of deadlocks, missing messages, and erroneous messaging order. In our previous work, we have proposed a set of composition operators, allowing designers to build realizable choreographies that are represented by conversation protocols (CPs). In this work, 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. In this paper, we show how our approach applies and scales to a set of use cases borrowed from the literature and used by the research community. We also show that our approach allows to detect failures and failure recovery in case realizability does not hold.

In this paper, we address the design of distributed systems composed of peers (state-transitions systems) communicating through message exchanges. We consider choreographies as the ground 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 does not require building the individual peers, nor their composition; they may be obtained by 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. In our previous work [1], we have proposed a set of composition operators allowing designers to build realizable choreographies that are represented by conversation protocols (CPs). We rely on the correct-by-construction Event-B method to prove that each CP constructed using our operators is realizable. In this paper, we show how our approach applies and scales to a set of use cases borrowed from the literature and used by the research community. We also show that our approach allows to detect failures and failure recovery in case realizability does not hold

Since software systems are becoming increasingly more concurrent and distributed, modeling and analysis of interactions among their components is a crucial problem. In several application domains, message-based communication is used as the interaction mechanism, and the communication contract among the components of the system is specified semantically as a state machine. In the service-oriented computing domain such communication contracts are called "choreography" specifications. A choreography specification identifies allowable ordering of message exchanges in a distributed system. A fundamental question about a choreography specification is determining its realizability, i.e., given a choreography specification, is it possible to build a distributed system that communicates exactly as the choreography specifies? Checking realizability of choreography specifications has been an open problem for several years and it was not known if this was a decidable problem. In this paper we give necessary and sufficient conditions for realizability of choreographies. We implemented the proposed realizability check and our experiments show that it can efficiently determine the realizability of 1) web service choreographies, 2) Singularity OS channel contracts, and 3) UML collaboration (communication) diagrams.

Adaptation is of utmost importance in systems developed by assembling reusable software services accessed through their public interfaces. This process aims at solving, as automatically as possible, mismatch cases which may be given at the different interoperability levels among interfaces by synthesizing a mediating adaptor. In this paper, we present a toolbox that fully supports the adaptation process, including: (i) different methods to construct adaptation contracts involving several services; (ii) simulation and verification techniques which help to identify and correct erroneous behaviours or deadlocking executions; and (iii) techniques for the generation of centralized or distributed adaptor protocols based on the aforementioned contracts. Our toolbox relates our models with implementation platforms, starting with the automatic extraction of behavioural models from existing interface descriptions, until the final adaptor implementation is generated for the target platform.