Model Checking the Pastry Routing Protocol - Archive ouverte HAL Access content directly
Conference Papers Year : 2010

Model Checking the Pastry Routing Protocol

(1) , (2) , (1)


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.
Fichier principal
Vignette du fichier
article-new.pdf (93.22 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

inria-00540811 , version 1 (29-11-2010)


  • 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⟩
256 View
388 Download


Gmail Facebook Twitter LinkedIn More