Chevrou, Florent and Hurault, Aurélie
and Nakajima, Shin and Quéinnec, Philippe
A Map of Asynchronous Communication Models.
(2019)
In: Refinement Workshop, in World Congress on Formal Methods (REFINE 2019), 7 October 2019 - 7 October 2019 (Porto, Portugal).
|
(Document in English)
PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader 573kB |
Abstract
Asynchronous communication encompasses a variety of fea-tures besides the decoupling of send and receive events. Those include message-ordering policies which are often crucial to the correctness of a distributed algorithm. This paper establishes a map of communica-tion models that exhibits the relations between them along two axes of comparison: the strength of the ordering property and the level of ab-straction of the specification. This brings knowledge about which model can be substituted by another without breaking any safety property. Fur-thermore, it brings flexibility and ready-to-use modules when developing correct-by-construction distributed systems where model decomposition exposes the communication component. Both criteria of comparison are covered by refinement. We consider seven ordering policies and we model in Event-B these communication models at three levels of abstraction. The proofs of refinement between all of these are mechanized in Rodin.
Item Type: | Conference or Workshop Item (Paper) |
---|---|
HAL Id: | hal-02930097 |
Audience (conference): | National conference proceedings |
Uncontrolled Keywords: | |
Institution: | French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE) Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE) Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE) Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE) Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE) Other partners > National Institute of Informatics - NII (JAPAN) |
Laboratory name: | |
Statistics: | download |
Deposited On: | 15 Jul 2020 12:34 |
Repository Staff Only: item control page