×

A modular framework for verifying versatile distributed systems. (English) Zbl 1435.68191

Summary: Putting independent components together is a common design practice of distributed systems. Besides, there exists a wide range of interaction protocols that dictate how these components interact, which impacts their compatibility. However, the communication model itself always consists in a monolithic description of the rules and properties of the communication. In this paper, we propose a mechanized framework for the compatibility checking of compositions of peers where the interaction protocol can be fine tuned through assembly of basic properties on the communication. These include whether the communication is point-to-point, multicast or convergecast, which ordering-policies are to be applied, applicative priorities, bounds on the number of messages in transit, and so on. Among these properties, we focus on a generic description of multicast communication that encompasses point-to-point and one-to-all communication as special cases. The components that form the communication model are specified in \(\mathrm{TLA}^+\), and a system, composed of a communication model and a specification of the behavior of the peers (also in \(\mathrm{TLA}^+\)), is checked with the \(\mathrm{TLA}^+\) model checker. Eventually we provide theoretical views on the relations between ordering-policies through the lenses of multicast and convergecast communication.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68M14 Distributed systems

Software:

SPIN; PlusCal; Horus; PSync; Verdi
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Allen, Robert; Garlan, David, Formalizing architectural connection, (16th International Conference on Software Engineering, ICSE ’94 (1994), IEEE Computer Society Press), 71-80
[2] Alur, Rajeev; Holzmann, Gerard J.; Peled, Doron, An analyzer for message sequence charts, (International Workshop on Tools and Algorithms for the Construction and Analysis of Systems. International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 1055 (1996), Springer), 35-48
[3] Aldini, Alessandro, Modeling and verification of trust and reputation systems, Secur. Commun. Netw., 8, 16, 2933-2946 (2015)
[4] Baeten, Jos C. M.; Bergstra, Jan A.; Klop, Jan Willem, Syntax and defining equations for an interrupt mechanism in process algebra, Fundam. Inform., IX, 127-168 (1986) · Zbl 0617.68027
[5] Basu, Samik; Bultan, Tevfik; Ouederni, Meriem, Deciding choreography realizability, (39th Symposium on Principles of Programming Languages, POPL ’12 (2012), ACM), 191-202 · Zbl 1321.68183
[6] Brogi, Antonio; Canal, Carlos; Pimentel, Ernesto; Vallecillo, Antonio, Formalizing web service choreographies, Electron. Notes Theor. Comput. Sci., 105, 73-94 (December 2004)
[7] Brand, Daniel; Zafiropulo, Pitro, On communicating finite-state machines, J. ACM, 30, 2, 323-342 (April 1983)
[8] Charron-Bost, Bernadette; Mattern, Friedemann; Tel, Gerard, Synchronous, asynchronous, and causally ordered communication, Distrib. Comput., 9, 4, 173-191 (February 1996)
[9] Charron-Bost, Bernadette; Schiper, André, The heard-of model: computing in distributed systems with benign faults, Distrib. Comput., 22, 1, 49-71 (April 2009)
[10] Cleaveland, Rance; Hennessy, Matthew, Priorities in process algebras, Inf. Comput., 87, 1/2, 58-77 (1990) · Zbl 0726.68053
[11] Chevrou, Florent; Hurault, Aurélie; Quéinnec, Philippe, On the diversity of asynchronous communication, Form. Asp. Comput., 28, 5, 847-879 (September 2016)
[12] Chevrou, Florent; Hurault, Aurélie; Quéinnec, Philippe, \(TLA^+\) modules for a modular framework for verifying versatile distributed systems (2019) · Zbl 1435.68191
[13] Camilleri, Juanito; Winskel, Glynn, CCS with priority choice, Inf. Comput., 116, 1, 26-37 (1995) · Zbl 0818.68107
[14] Drăgoi, Cezara; Henzinger, Thomas A.; Psync, Damien Zufferey, A partially synchronous language for fault-tolerant distributed algorithms, (43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’16 (2016), ACM), 400-415 · Zbl 1347.68036
[15] Durán, Francisco; Ouederni, Meriem; Salaün, Gwen, A generic framework for n-protocol compatibility checking, Sci. Comput. Program., 77, 7-8, 870-886 (July 2012)
[16] Engels, André; Mauw, Sjouke; Reniers, Michel A., A hierarchy of communication models for message sequence charts, Sci. Comput. Program., 44, 3, 253-292 (2002) · Zbl 1014.68040
[17] Garlan, David; Monroe, Robert; Acme, David Wile, An architecture description interchange language, (CASCON’97 (1997)), 169-183
[18] Hickey, Jason J.; Lynch, Nancy; van Renesse, Robbert, Specifications and proofs for Ensemble layers, (Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’99). Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’99), LNCS, vol. 1579 (1999), Springer-Verlag), 119-133
[19] Holzmann, Gerard J., The Spin Model Checker: Primer and Reference Manual (2004), Addison-Wesley
[20] Hull, M. Elizabeth C., Occam - a programming language for multiprocessor systems, Comput. Lang., 12, 1, 27-37 (1987) · Zbl 0614.68027
[21] Kshemkalyani, Ajay D.; Singhal, Mukesh, Distributed Computing: Principles, Algorithms, and Systems (March 2011), Cambridge University Press
[22] Lamport, Leslie, Time, clocks and the ordering of events in a distributed system, Commun. ACM, 21, 7, 558-565 (July 1978)
[23] Lamport, Leslie, Specifying Systems (2002), Addison Wesley · Zbl 0959.68080
[24] Lamport, Leslie, The PlusCal algorithm language, (Theoretical Aspects of Computing - ICTAC 2009, 6th International Colloquium. Theoretical Aspects of Computing - ICTAC 2009, 6th International Colloquium, Lecture Notes in Computer Science, vol. 5684 (2009), Springer), 36-60 · Zbl 1250.68284
[25] Liu, Xiaoming; Kreitz, Christoph; van Renesse, Robbert; Hickey, Jason J.; Hayden, Mark; Birman, Kenneth; Constable, Robert, Building reliable, high-performance communication systems from components, (17th ACM Symposium on Operating Systems Principles (SOSP’99). 17th ACM Symposium on Operating Systems Principles (SOSP’99), Operating Systems Review, vol. 33(5) (December 1999), ACM Press), 80-92
[26] Li, Xiaozhou; Misra, Jayadev; Plaxton, C. Greg, Active and concurrent topology maintenance, (Distributed Computing, 18th International Conference. Distributed Computing, 18th International Conference, Lecture Notes in Computer Science, vol. 3274 (2004), Springer), 320-334 · Zbl 1110.68324
[27] Lynch, Nancy A., Distributed Algorithms (1996), Morgan Kaufmann Publishers Inc. · Zbl 0877.68061
[28] Mauw, Sjouke; Reniers, Michel A., An algebraic semantics of basic message sequence charts, Comput. J., 37, 4, 269-277 (1994)
[29] van Renesse, Robbert; Birman, Kenneth P.; Hayden, Mark; Vaysburd, Alexey; Karr, David, Building adaptive systems using Ensemble, Softw. Pract. Exp., 28, 9, 963-979 (August 1998)
[30] van Renesse, Robbert; Birman, Kenneth P.; Horus, Silvano Maffeis, A flexible group communications system, Commun. ACM, 39, 4, 76-83 (April 1996)
[31] Segall, A., Distributed network protocols, IEEE Trans. Inf. Theory, 29, 1, 23-35 (1983) · Zbl 0531.94026
[32] Tel, Gerard, Introduction to Distributed Algorithms (2000), Cambridge University Press · Zbl 0961.68157
[33] Taylor, R. N.; Medvidovic, N.; Anderson, K. M.; Whitehead, E. J.; Robbins, J. E.; Nies, K. A.; Oreizy, P.; Dubrow, D. L., A component- and message-based architectural style for GUI software, IEEE Trans. Softw. Eng., 22, 6, 390-406 (June 1996)
[34] Wilcox, James R.; Woos, Doug; Panchekha, Pavel; Tatlock, Zachary; Wang, Xi; Ernst, Michael D.; Verdi, Thomas Anderson, A framework for implementing and formally verifying distributed system, (36th ACM Conference on Programming Language Design and Implementation (June 2015)), 357-368
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.