Choreographies prescribe the rendez-vous synchronisation of messages in a communicating system. Such a system is called realisable, if the traces of the prescribed communication coincide with those of the asynchronous system of peers, where the communication channels either use FIFO queues or multiset mailboxes. It has recently been shown that realisability can be characterised by two necessary conditions that together are also sufficient, whereas in general the synchronisability of communicating peers is undecidable. The sufficiency of the conditions permits the construction of correct communicating systems; their necessity shows that all choreography-defined communicating system can be obtained in this way. This article provides an integrated framework based on Event-B for such a construction with a major emphasis on Rodin-based proofs of correctness and completeness.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{BenyagoubAS20,
author = {Sarah Benyagoub and
Yamine A{\"{\i}}t Ameur and
Klaus{-}Dieter Schewe},
editor = {Alexander Raschke and
Dominique M{\'{e}}ry and
Frank Houdek},
title = {Event-B-Supported Choreography-Defined Communicating Systems - Correctness
and Completeness},
booktitle = {Rigorous State-Based Methods - 7th International Conference, {ABZ}
2020, Ulm, Germany, May 27-29, 2020, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {12071},
pages = {155--168},
publisher = {Springer},
year = {2020},
url = {https://doi.org/10.1007/978-3-030-48077-6\_11},
doi = {10.1007/978-3-030-48077-6\_11},
timestamp = {Mon, 25 May 2020 12:33:39 +0200},
biburl = {https://dblp.org/rec/conf/asm/BenyagoubAS20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}