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 metadatas

https://hal.inria.fr/inria-00540811
Contributor : Stephan Merz <>
Submitted on : Monday, November 29, 2010 - 11:51:40 AM
Last modification on : Thursday, February 21, 2019 - 2:02:02 PM
Long-term archiving on : Friday, December 2, 2016 - 5:49:26 PM

File

article-new.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00540811, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

430

Files downloads

535