Verifying a Structured Peer-to-Peer Overlay Network: The Static Case

  • Johannes Borgström
  • Uwe Nestmann
  • Luc Onana
  • Dilian Gurov
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3267)


Structured peer-to-peer overlay networks are a class of algorithms that provide e.cient message routing for distributed applications using a sparsely connected communication network. In this paper, we formally verify a typical application running on a .xed set of nodes. This work is the foundation for studies of a more dynamic system.

We identify a value and expression language for a value-passing CCS that allows us to formally model a distributed hash table implemented over a static DKS overlay network. We then provide a speci.cation of the lookup operation in the same language, allowing us to formally verify the correctness of the system in terms of observational equivalence between implementation and speci.cation. For the proof, we employ an abstract notation for reachable states that allows us to work conveniently up to structural congruence, thus drastically reducing the number and shape of states to consider. The structure and techniques of the correctness proof are reusable for other overlay networks.


Overlay Network Transition Graph Distribute Hash Table Reachable State Label Transition System 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [AG99]
    Abadi, M., Gordon, A.D.: A Calculus for Cryptographic Protocols: The Spi Calculus. Information and Computation 148(1), 1–70 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  2. [BH00]
    Berger, M., Honda, K.: The Two-Phase Commitment Protocol in an Extended pi-Calculus. In: Aceto, L., Victor, B. (eds.) Proceedings of EXPRESS 2000. ENTCS, vol. 39.1. Elsevier Science Publishers, Amsterdam (2000)Google Scholar
  3. [Gos91]
    Goscinski, A.: Distributed Operating Systems, The Logical Design. Addison-Wesley, Reading (1991)Google Scholar
  4. [Ing94]
    Ingólfsdóttir, A.: Semantic Models for Communicating Processes with Value-Passing. PhD thesis, University of Sussex, Available as Technical Report 8/94 (1994)Google Scholar
  5. [LT98]
    Lynch, N.A., Tuttle, M.R.: An Introduction to Input/Output Automata. Technical Report MIT/LCS/TM 373. MIT Press, Redmond (1998)Google Scholar
  6. [Mil89]
    Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)zbMATHGoogle Scholar
  7. [MPW92]
    Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes, Part I/II. Information and Computation 100, 1–77 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  8. [NFM03]
    Nestmann, U., Fuzzati, R., Merro, M.: Modeling Consensus in a Process Calculus. In: Amadio, R., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 399–414. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  9. [OEBH03]
    Onana Alima, L., El-Ansary, S., Brand, P., Haridi, S.: DKS (N, k, f): A Family of Low Communication, Scalable and Fault-Tolerant Infrastructures for P2P Applications. In: CCGRID 2003, pp. 344–350 (2003)Google Scholar
  10. [OGEA+03]
    Onana Alima, L., Ghodsi, A., El-Ansary, S., Brand, P., Haridi, S.: Design Principles for Structured Overlay Networks. Technical Report ISRN KTH/IMIT/LECS/R-03/01–SE, KTH (2003)Google Scholar
  11. [RD01]
    Rowstron, A., Druschel, P.: Pastry: Scalable, distributed object location and routing for large-scale peer-to-peer systems. In: Guerraoui, R. (ed.) Middleware 2001. LNCS, vol. 2218, pp. 329–350. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  12. [RFH+01]
    Ratnasamy, S., Francis, P., Handley, M., Karp, R., Shenker, S.: A Scalable Content Addressable Network. In: SIGCOMM 2001. ACM, San Diego (2001)Google Scholar
  13. [SMK+01]
    Stoica, I., Morris, R., Karger, D., Kaashoek, M.F., Balakrishnan, H.: Chord: A Scalable Peer-to-peer Lookup Service for Internet Applications. In: SIGCOMM 2001. ACM Press, San Diego (2001)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Johannes Borgström
    • 1
  • Uwe Nestmann
    • 1
  • Luc Onana
    • 2
    • 3
  • Dilian Gurov
    • 2
    • 3
  1. 1.School of Computer and Communication SciencesEPFLSwitzerland
  2. 2.Department of Microelectronics and Information TechnologyKTHSweden
  3. 3.SICSSweden

Personalised recommendations