Formal Verification Of Pastry Using TLA+

Abstract : Pastry is an algorithm that provides a scalable distributed hash table over an underlying P2P network. Several implementations of Pastry are available, but to the best of our knowledge the correctness of the algorithm has not been verified formally. Since Pastry combines rather complex data structures, asynchronous communication, concurrency, resilience to churn and fault tolerance, we believe that it makes an interesting target for verification using TLA+. More precisely, our goal is to model the join and lookup protocols of Pastry using the TLA+ language, and to use the associated tools to verify significant correctness properties.
Type de document :
Communication dans un congrès
Leslie Lamport and Stephan Merz. International Workshop on the TLA+ Method and Tools, Aug 2012, Paris, France. 2012
Liste complète des métadonnées

Littérature citée [6 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00768812
Contributeur : Stephan Merz <>
Soumis le : lundi 24 décembre 2012 - 11:43:56
Dernière modification le : jeudi 11 janvier 2018 - 06:25:25
Document(s) archivé(s) le : lundi 25 mars 2013 - 03:50:33

Fichiers

paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00768812, version 1

Collections

Citation

Tianxiang Lu, Stephan Merz, Christoph Weidenbach. Formal Verification Of Pastry Using TLA+. Leslie Lamport and Stephan Merz. International Workshop on the TLA+ Method and Tools, Aug 2012, Paris, France. 2012. 〈hal-00768812〉

Partager

Métriques

Consultations de la notice

361

Téléchargements de fichiers

419