Formal design of scalable conversation protocols using Event‐B: Validation, experiments, and benchmarks. Issue 2 (12th December 2019)

• Record Type: Journal Article
• Authors: Benyagoub, Sarah; Aït‐Ameur, Yamine; Ouederni, Meriem; Mashkoor, Atif; Medeghri, Ahmed
• Other Names: Mashkoor Atif guestEditor.; Sametinger Johannes guestEditor.; Biro Miklós guestEditor.; Egyed Alexander guestEditor.
• Is Part Of: Journal of software. Volume 32:Issue 2(2020)
• Page Start: n/a
• Page End: n/a
• Publication Date: 2019-12-12
• Subjects: choreography realizability -- conversation protocols -- correct by construction -- distributed systems -- Event‐B -- proof and refinement‐based methods; Software engineering -- Periodicals; Computer software -- Development -- Periodicals; Software maintenance -- Periodicals; 005.1
• DOI: 10.1002/smr.2209
• Languages: English
• ISSNs: 2047-7473

Abstract

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.