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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Charron-Bost, B., Mattern, F., Tel, G.: Synchronous, asynchronous, and causally ordered communication. Distrib. Comput. 9(4), 173–191 (1996)
Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: Verifying safety properties with the TLA\(^{+}\) proof system. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 142–148. Springer, Heidelberg (2010)
Chevrou, F., Hurault, A., Quéinnec, P.: Automated verification of asynchronous communicating systems with TLA+. In: Electronic Communications of the EASST (PostProceedings of the 15th International Workshop on Automated Verification of Critical Systems), vol. 72, pp. 1–15 (2015)
Kshemkalyani, A.D., Singhal, M.: Distributed Computing: Principles, Algorithms, and Systems. Cambridge University Press, Cambridge (2011)
Lamport, L.: Time, clocks and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)
Lamport, L.: Specifying Systems. Addison Wesley, Reading (2002)
Tel, G.: Introduction to Distributed Algorithms, 2nd edn. Cambridge University Press, Cambridge (2000)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Chevrou, F., Hurault, A., Mauran, P., Quéinnec, P. (2016). Mechanized Refinement of Communication Models with TLA\(^+\) . In: Butler, M., Schewe, KD., Mashkoor, A., Biro, M. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2016. Lecture Notes in Computer Science(), vol 9675. Springer, Cham. https://doi.org/10.1007/978-3-319-33600-8_27
Download citation
DOI: https://doi.org/10.1007/978-3-319-33600-8_27
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-33599-5
Online ISBN: 978-3-319-33600-8
eBook Packages: Computer ScienceComputer Science (R0)