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.

Document

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.

Reference

% BibTex
@inproceedings{ChevrouHMQ16,
  author       = {Florent Chevrou and
                  Aur{\'{e}}lie Hurault and
                  Philippe Mauran and
                  Philippe Qu{\'{e}}innec},
  editor       = {Michael J. Butler and
                  Klaus{-}Dieter Schewe and
                  Atif Mashkoor and
                  Mikl{\'{o}}s Bir{\'{o}}},
  title        = {Mechanized Refinement of Communication Models with {TLA} {\^{}}+ +},
  booktitle    = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 5th International
                  Conference, {ABZ} 2016, Linz, Austria, May 23-27, 2016, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {9675},
  pages        = {312--318},
  publisher    = {Springer},
  year         = {2016},
  url          = {https://doi.org/10.1007/978-3-319-33600-8\_27},
  doi          = {10.1007/978-3-319-33600-8\_27},
  timestamp    = {Tue, 14 May 2019 10:00:50 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/ChevrouHMQ16.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}