Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


Towards verification of the pastry protocol using TLA+

Lu, Tianxiang and Merz, Stephan and Weidenbach, Christoph

MPI-I-2011-RG1-002. June 2011, 51 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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 verication. We have modeled Pastry's core routing algorithms and communication
protocol in the specication 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 rst result is the reduction of global
Pastry correctness properties to invariants of the underlying data structures.
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-2011-RG1-002.pdfMPI-I-2011-RG1-002.pdf423 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document:
Hide details for BibTeXBibTeX
  AUTHOR = {Lu, Tianxiang and Merz, Stephan and Weidenbach, Christoph},
  TITLE = {Towards verification of the pastry protocol using {TLA+}},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Stuhlsatzenhausweg 85, 66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-2011-RG1-002},
  MONTH = {June},
  YEAR = {2011},
  ISSN = {0946-011X},