Skip to Main content Skip to Navigation
Conference papers

Mechanized Refinement of Communication Models with TLA+

Abstract : In distributed systems, asynchronous communication is often viewed as a whole whereas there are actually many different interaction protocols whose properties are involved in the compatibility of peer compositions. A hierarchy of asynchronous communication models, based on refinements, is established and proven with the TLA+ Proof System. The work serves as a first step in the study of the substituability of the communication models when it comes to compatibility checking.
Complete list of metadata

Cited literature [4 references]  Display  Hide  Download
Contributor : Open Archive Toulouse Archive Ouverte (oatao) <>
Submitted on : Friday, June 9, 2017 - 5:28:11 PM
Last modification on : Thursday, March 18, 2021 - 2:34:37 PM
Long-term archiving on: : Sunday, September 10, 2017 - 1:33:02 PM


Files produced by the author(s)


  • HAL Id : hal-01535944, version 1
  • OATAO : 16917


Florent Chevrou, Aurélie Hurault, Philippe Mauran, Philippe Quéinnec. Mechanized Refinement of Communication Models with TLA+. 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2016), May 2016, Linz, Austria. pp. 312-318. ⟨hal-01535944⟩



Record views


Files downloads