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.
CITATION STYLE
Chevrou, F., Hurault, A., Mauran, P., & Quéinnec, P. (2016). Mechanized refinement of communication models with TLA+. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9675, pp. 312–318). Springer Verlag. https://doi.org/10.1007/978-3-319-33600-8_27
Mendeley helps you to discover research relevant for your work.