Abstract
Formal reasoning on Peer-to-Peer (P2P) systems is an intimidating task. This paper focuses on broadcast algorithms for Content Addressable Network (CAN). Since these algorithms run on top of complex P2P systems, finding the right level of abstraction in order to prove their functional correctness is difficult. This paper presents a mechanized model for both CAN and broadcast protocols over those networks. We demonstrate that our approach is practical by identifying sufficient conditions for a protocol to be correct and efficient. We also prove the existence of a protocol verifying those properties.
Chapter PDF
Similar content being viewed by others
References
Bakhshi, R., Gurov, D.: Verification of peer-to-peer algorithms: A case study. Electronic Notes in Theoretical Computer Science 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)
Charron-Bost, B., Merz, S.: Formal verification of a consensus algorithm in the heard-of model. Int. J. Software and Informatics 3(2-3) (2009)
DeCandia, G., Hastorun, D., Jampani, M., Kakulapati, G., Lakshman, A., Pilchin, A., Sivasubramanian, S., Vosshall, P., Vogels, W.: Dynamo: amazon’s highly available key-value store. In: SOSP, pp. 205–220. ACM (2007)
Guo, H., Wu, M., Zhou, L., Hu, G., Yang, J., Zhang, L.: Practical software model checking via dynamic interface reduction. In: SOSP, pp. 265–278. ACM (2011)
Gupta, A., Sahin, O.D., Agrawal, D.P., El Abbadi, A.: Meghdoot: Content-Based Publish/Subscribe over P2P Networks. In: Jacobsen, H.-A. (ed.) Middleware 2004. LNCS, vol. 3231, pp. 254–273. Springer, Heidelberg (2004)
Haiyan, Q.: Testing and Proving Distributed Algorithms in Constructive Type Theory. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 79–94. Springer, Heidelberg (2007)
Hu, S.Y., Chen, J.F., Chen, T.H.: VON: a scalable peer-to-peer network for virtual environments. IEEE Network 20(4), 22–31 (2006)
Lakshman, A., Malik, P.: Cassandra: a decentralized structured storage system. SIGOPS Oper. Syst. Rev. 44(2), 35–40 (2010)
Liebeherr, J., Nahas, M., Si, W.: Application-layer multicasting with delaunay triangulation overlays. IEEE Journal on Selected Areas in Communications 20(8), 1472–1488 (2002)
Lu, T., Merz, S., Weidenbach, C.: Towards Verification of the Pastry Protocol Using TLA + . In: Bruni, R., Dingel, J. (eds.) FORTE 2011 and FMOODS 2011. LNCS, vol. 6722, pp. 244–258. Springer, Heidelberg (2011)
Merz, S., Vanzetto, H.: Automatic Verification of TLA +  Proof Obligations with SMT Solvers. In: Bjørner, N., Voronkov, A. (eds.) LPAR-18 . LNCS, vol. 7180, pp. 289–303. Springer, Heidelberg (2012)
Nipkow, T., Paulson, L.C., Wenzel, M.T. (eds.):Isabelle/HOL: a proof assistant for higher-order logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
Ratnasamy, S., Francis, P., Handley, M., Karp, R., Shenker, S.: A Scalable Content-Addressable Network. In: SIGCOMM, pp. 161–172. ACM (2001)
Ratnasamy, S., Handley, M., Karp, R.M., Shenker, S.: Application-Level Multicast Using Content-Addressable Networks. In: Crowcroft, J., Hofmann, M. (eds.) NGC 2001. LNCS, vol. 2233, pp. 14–29. Springer, Heidelberg (2001)
Ridge, T., Norrish, M., Sewell, P.: A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 294–309. Springer, Heidelberg (2008)
Ridge, T.: Verifying distributed systems: the operational approach. In: POPL, Savannah, GA, USA, p. 429 (2009)
Chou, C.T.: Mechanical verification of distributed algorithms in higher-order logic. The Computer Journal 38(2), 152 (1995)
Zave, P.: Using lightweight modeling to understand chord. Computer Communication Review 42(2), 49–57 (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bongiovanni, F., Henrio, L. (2013). A Mechanized Model for CAN Protocols. In: Cortellessa, V., Varró, D. (eds) Fundamental Approaches to Software Engineering. FASE 2013. Lecture Notes in Computer Science, vol 7793. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37057-1_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-37057-1_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-37056-4
Online ISBN: 978-3-642-37057-1
eBook Packages: Computer ScienceComputer Science (R0)