{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T05:46:20Z","timestamp":1749793580561,"version":"3.40.3"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319259413"},{"type":"electronic","value":"9783319259420"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-25942-0_19","type":"book-chapter","created":{"date-parts":[[2015,10,16]],"date-time":"2015-10-16T05:32:14Z","timestamp":1444973534000},"page":"284-299","source":"Crossref","is-referenced-by-count":3,"title":["Formal Verification of the Pastry Protocol Using $$\\mathrm{{TLA}}^{+}$$"],"prefix":"10.1007","author":[{"given":"Tianxiang","family":"Lu","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,10,17]]},"reference":[{"key":"19_CR1","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.entcs.2007.01.052","volume":"181","author":"R Bakhshi","year":"2007","unstructured":"Bakhshi, R., Gurov, D.: Verification of peer-to-peer algorithms: A case study. Electr. Notes Theor. Comput. Sci. 181, 35\u201347 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-540-31794-4_13","volume-title":"Global Computing","author":"J Borgstr\u00f6m","year":"2005","unstructured":"Borgstr\u00f6m, 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\u2013265. Springer, Heidelberg (2005)"},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"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\u201318. IEEE Computer Society, Florence (2004)","DOI":"10.1109\/DSN.2004.1311872"},{"key":"19_CR4","unstructured":"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"},{"issue":"3","key":"19_CR5","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1145\/945721.945730","volume":"32","author":"JM Hellerstein","year":"2003","unstructured":"Hellerstein, J.M.: Toward network data independence. ACM SIGMOD Record 32(3), 34\u201340 (2003)","journal-title":"ACM SIGMOD Record"},{"key":"19_CR6","unstructured":"Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002)"},{"key":"19_CR7","unstructured":"Lamport, L.: TLA tools (2012). \n                      http:\/\/www.tlaplus.net\/"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/978-3-540-30186-8_23","volume-title":"Distributed Computing","author":"X Li","year":"2004","unstructured":"Li, X., Misra, J., Plaxton, C.G.: Active and Concurrent Topology Maintenance. In: Guerraoui, R. (ed.) DISC 2004. LNCS, vol. 3274, pp. 320\u2013334. Springer, Heidelberg (2004)"},{"key":"19_CR9","unstructured":"Lu, T.: Formal Verification of the Pastry Protocol. Ph.D. thesis, Universit\u00e4t des Saarlandes, Saarbr\u00fccken (2013). \n                      urn:nbn:de:bsz:291-scidok-55878"},{"key":"19_CR10","unstructured":"Lu, T.: The TLA+ codes for the pastry model (2013). \n                      http:\/\/tiit.lu\/fmPastry\/"},{"key":"19_CR11","unstructured":"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\u201321. Universit\u00e4t D\u00fcseldorf, D\u00fcsseldorf, Germany (2010)"},{"key":"19_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-21461-5_16","volume-title":"Formal Techniques for Distributed Systems","author":"T Lu","year":"2011","unstructured":"Lu, T., Merz, S., Weidenbach, C.: Towards verification of the pastry protocol using TLA\n                      \n                        \n                      \n                      $$^ \\text{+ } $$\n                    . In: Bruni, R., Dingel, J. (eds.) FORTE 2011 and FMOODS 2011. LNCS, vol. 6722, pp. 244\u2013258. Springer, Heidelberg (2011)"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Lu, T., Merz, S., Weidenbach, C.: Formal verification of the pastry protocol using TLA+. 18th International Symposium on Formal Methods (2012)","DOI":"10.1007\/978-3-642-21461-5_16"},{"key":"19_CR14","unstructured":"Lynch, N., Stoica, I.: Multichord: A resilient namespace management protocol. MIT CSAIL Technical Report (2004)"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"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\u201325. IEEE (2005)","DOI":"10.1109\/LCN.2005.69"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/3-540-45518-3_18","volume-title":"Middleware 2001","author":"A Rowstron","year":"2001","unstructured":"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)"},{"issue":"4","key":"19_CR17","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1145\/964723.383071","volume":"31","author":"I Stoica","year":"2001","unstructured":"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\u2013160 (2001). ACM","journal-title":"ACM SIGCOMM Computer Communication Review"},{"issue":"2","key":"19_CR18","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1145\/2185376.2185383","volume":"42","author":"P Zave","year":"2012","unstructured":"Zave, P.: Using lightweight modeling to understand chord. Computer Communication Review 42(2), 49\u201357 (2012)","journal-title":"Computer Communication Review"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering: Theories, Tools, and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25942-0_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T03:08:09Z","timestamp":1559272089000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25942-0_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319259413","9783319259420"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25942-0_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}