Towards Verification of the Pastry Protocol Using TLA + 

Tianxiang Lu 1, 2 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 that provides a scalable distributed hash table over an underlying P2P network. 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 and communication protocol in the specification language TLA + . In order to validate the model and to search for bugs we employed the TLA +  model checker tlc to analyze several qualitative properties. We obtained non-trivial insights in the behavior of Pastry through the model checking analysis. Furthermore, we started to verify Pastry using the very same model and the interactive theorem prover tlaps for TLA + . A first result is the reduction of global Pastry correctness properties to invariants of the underlying data structures.
Complete list of metadatas

Cited literature [10 references]  Display  Hide  Download

https://hal.inria.fr/hal-01583322
Contributor : Hal Ifip <>
Submitted on : Thursday, September 7, 2017 - 11:10:21 AM
Last modification on : Thursday, February 21, 2019 - 2:02:02 PM

File

978-3-642-21461-5_16_Chapter.p...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Tianxiang Lu, Stephan Merz, Christoph Weidenbach. Towards Verification of the Pastry Protocol Using TLA + . 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik, Iceland. pp.244-258, ⟨10.1007/978-3-642-21461-5_16⟩. ⟨hal-01583322⟩

Share

Metrics

Record views

285

Files downloads

191