Towards Verification of the Pastry Protocol using TLA+

Stephan Merz 1, 2, 3 Tianxiang Lu 4 Christoph Weidenbach 4
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
2 MOSEL - Proof-oriented development of computer-based systems
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
3 MSR - INRIA - Microsoft Research - Inria Joint Centre
4 MPII - Max-Planck-Institut für Informatik
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.
Keywords : formal specification model checking verification methods network protocols
Type de document :
Communication dans un congrès
R. Bruni and J. Dingel. 31st IFIP International Conference on Formal Techniques for Networked and Distributed Systems, Jun 2011, Reykjavik, Iceland. 6722, 2011, FMOODS/FORTE 2011
Liste complète des métadonnées
https://hal.inria.fr/inria-00593523
Contributeur : Stephan Merz <>
Soumis le : lundi 16 mai 2011 - 14:00:18
Dernière modification le : jeudi 11 janvier 2018 - 06:23:25

Identifiants

  • HAL Id : inria-00593523, version 1

Collections

INRIA | UNIV-LORRAINE | LORIA-FM | LORIA

Citation

Stephan Merz, Tianxiang Lu, Christoph Weidenbach. Towards Verification of the Pastry Protocol using TLA+. R. Bruni and J. Dingel. 31st IFIP International Conference on Formal Techniques for Networked and Distributed Systems, Jun 2011, Reykjavik, Iceland. 6722, 2011, FMOODS/FORTE 2011. 〈inria-00593523〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

185

Contact


archive-ouverte@inria.fr