2011 | OriginalPaper | Buchkapitel
Towards Verification of the Pastry Protocol Using TLA +
verfasst von : Tianxiang Lu, Stephan Merz, Christoph Weidenbach
Erschienen in: Formal Techniques for Distributed Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.