A Map of Asynchronous Communication Models

Florent Chevrou (1) , Aurélie Hurault (1, 2) , Shin Nakajima (3) , Philippe Quéinnec (1)

1 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
2 Toulouse INP - Institut National Polytechnique (Toulouse)
3 NII - National Institute of Informatics

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.

Mots clés: Asynchronous communication; formal verification; refine-ments of communication models; Event-B

Domaines: Génie logiciel [cs.SE]; Systèmes embarqués; Cryptographie et sécurité [cs.CR]; Interface homme-machine [cs.HC]; Architectures Matérielles [cs.AR]; Modélisation et simulation

Florent Chevrou, Aurélie Hurault, Shin Nakajima, Philippe Quéinnec. A Map of Asynchronous Communication Models. Refinement Workshop, in World Congress on Formal Methods (REFINE 2019), Oct 2019, Porto, Portugal. pp.1-15, ⟨10.1007/978-3-030-54997-8_20⟩. ⟨hal-02930097⟩