Abstract
As a consequence of the rise of cloud computing, the reliability of network protocols is gaining increasing attention. However, formal methods have revealed inconsistencies in some of these protocols, e.g., Chord, where all published versions of the protocol have been discovered to be incorrect. Pastry is a protocol similar to Chord. Using \(\mathrm{{TLA}}^{+}\), a formal specification language, we show that LuPastry, a formal model of Pastry with some improvements, provides correct delivery service. This is the first formal proof of Pastry where concurrent joins and lookups are simultaneously allowed. In particular, this article relaxes the assumption from previous publication to allow arbitrary concurrent joins of nodes, which reveals new insights into Pastry through a final formal model in \(\mathrm{{TLA}}^{+}\), LuPastry. Besides, this article also illustrates the methodology for the discovery and proof of its invariant. The proof in \(\mathrm{{TLA}}^{+}\) is mechanically verified using the interactive theorem prover TLAPS.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Bakhshi, R., Gurov, D.: Verification of peer-to-peer algorithms: A case study. Electr. Notes Theor. Comput. Sci. 181, 35–47 (2007)
Borgström, J., Nestmann, U., Onana, L., Gurov, D.: Verifying a structured peer-to-peer overlay network: the static case. In: Priami, C., Quaglia, P. (eds.) GC 2004. LNCS, vol. 3267, pp. 250–265. Springer, Heidelberg (2005)
Castro, M., Costa, M., Rowstron, A.I.T.: Performance and dependability of structured peer-to-peer overlays. In: International Conference on Dependable Systems and Networks (DSN 2004), pp. 9–18. IEEE Computer Society, Florence (2004)
Haeberlen, A., Hoye, J., Mislove, A., Druschel, P.: Consistent key mapping in structured overlays. Tech. Rep. TR05-456, Rice University, Department of Computer Science, August 2005
Hellerstein, J.M.: Toward network data independence. ACM SIGMOD Record 32(3), 34–40 (2003)
Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002)
Lamport, L.: TLA tools (2012). http://www.tlaplus.net/
Li, X., Misra, J., Plaxton, C.G.: Active and Concurrent Topology Maintenance. In: Guerraoui, R. (ed.) DISC 2004. LNCS, vol. 3274, pp. 320–334. Springer, Heidelberg (2004)
Lu, T.: Formal Verification of the Pastry Protocol. Ph.D. thesis, Universität des Saarlandes, Saarbrücken (2013). urn:nbn:de:bsz:291-scidok-55878
Lu, T.: The TLA+ codes for the pastry model (2013). http://tiit.lu/fmPastry/
Lu, T., Merz, S., Weidenbach, C.: Model checking the Pastry routing protocol. In: Bendisposto, J., Leuschel, M., Roggenbach, M. (eds.) 10th Intl. Workshop Automatic Verification of Critical Systems (AVOCS), pp. 19–21. Universität Düseldorf, Düsseldorf, Germany (2010)
Lu, T., Merz, S., Weidenbach, C.: Towards verification of the pastry protocol using TLA\(^ \text{+ } \). In: Bruni, R., Dingel, J. (eds.) FORTE 2011 and FMOODS 2011. LNCS, vol. 6722, pp. 244–258. Springer, Heidelberg (2011)
Lu, T., Merz, S., Weidenbach, C.: Formal verification of the pastry protocol using TLA+. 18th International Symposium on Formal Methods (2012)
Lynch, N., Stoica, I.: Multichord: A resilient namespace management protocol. MIT CSAIL Technical Report (2004)
Risson, J., Robinson, K., Moors, T.: Fault tolerant active rings for structured peer-to-peer overlays. In: The IEEE Conference on Local Computer Networks, 30th Anniversary 2005, pp. 18–25. IEEE (2005)
Rowstron, A., Druschel, P.: Pastry: scalable, decentralized object location, and routing for large-scale peer-to-peer systems. In: Guerraoui, R. (ed.) Middleware 2001. LNCS, vol. 2218, p. 329. Springer, Heidelberg (2001)
Stoica, I., Morris, R., Karger, D., Kaashoek, M.F., Balakrishnan, H.: Chord: A scalable peer-to-peer lookup service for internet applications. ACM SIGCOMM Computer Communication Review 31(4), 149–160 (2001). ACM
Zave, P.: Using lightweight modeling to understand chord. Computer Communication Review 42(2), 49–57 (2012)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Lu, T. (2015). Formal Verification of the Pastry Protocol Using \(\mathrm{{TLA}}^{+}\) . In: Li, X., Liu, Z., Yi, W. (eds) Dependable Software Engineering: Theories, Tools, and Applications. SETTA 2015. Lecture Notes in Computer Science(), vol 9409. Springer, Cham. https://doi.org/10.1007/978-3-319-25942-0_19
Download citation
DOI: https://doi.org/10.1007/978-3-319-25942-0_19
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-25941-3
Online ISBN: 978-3-319-25942-0
eBook Packages: Computer ScienceComputer Science (R0)