Skip to Main content Skip to Navigation
Conference papers

Model Checking the Pastry Routing Protocol

Tianxiang Lu 1 Stephan Merz 2 Christoph Weidenbach 1
2 VERIDIS - VERIfication pour les systèmes DIStribués
Inria Nancy - Grand Est, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications : UMR7503
Abstract : Pastry is an algorithm for implementing a scalable distributed hash table over an underlying P2P network, an active area of research in distributed systems. Several implementations of Pastry are available and have been applied in practice, but no attempt has so far been made to formally describe the algorithm or to verify its properties. Since Pastry combines rather complex data structures, asynchronous communication, concurrency, resilience to churn and fault tolerance, it makes an interesting target for verification. We have modeled Pastry's core routing algorithms in the specification language TLA+ and used its model checker TLC to analyze qualitative properties of Pastry such as correctness and consistency.
Document type :
Conference papers
Complete list of metadata
Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Monday, November 29, 2010 - 11:51:40 AM
Last modification on : Saturday, October 16, 2021 - 11:26:10 AM
Long-term archiving on: : Friday, December 2, 2016 - 5:49:26 PM


Files produced by the author(s)


  • HAL Id : inria-00540811, version 1



Tianxiang Lu, Stephan Merz, Christoph Weidenbach. Model Checking the Pastry Routing Protocol. 10th International Workshop Automated Verification of Critical Systems, Sep 2010, Düsseldorf, Germany. pp.19-21. ⟨inria-00540811⟩



Record views


Files downloads