Model Checking the Pastry Routing Protocol

Abstract : Pastry is an algorithm for implementing a scalable distributed hash table over an underlying P2P network, an active area of research in distributed systems. 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 in the specification language TLA+ and used its model checker TLC to analyze qualitative properties of Pastry such as correctness and consistency.
Type de document :
Communication dans un congrès
Jens Bendisposto and Michael Leuschel and Markus Roggenbach. 10th International Workshop Automated Verification of Critical Systems, Sep 2010, Düsseldorf, Germany. Universität Düsseldorf, pp.19-21, 2010, 10th International Workshop Automated Verification of Critical Systems
Liste complète des métadonnées

https://hal.inria.fr/inria-00540811
Contributeur : Stephan Merz <>
Soumis le : lundi 29 novembre 2010 - 11:51:40
Dernière modification le : mardi 18 décembre 2018 - 16:38:25
Document(s) archivé(s) le : vendredi 2 décembre 2016 - 17:49:26

Fichier

article-new.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00540811, version 1

Collections

Citation

Tianxiang Lu, Stephan Merz, Christoph Weidenbach. Model Checking the Pastry Routing Protocol. Jens Bendisposto and Michael Leuschel and Markus Roggenbach. 10th International Workshop Automated Verification of Critical Systems, Sep 2010, Düsseldorf, Germany. Universität Düsseldorf, pp.19-21, 2010, 10th International Workshop Automated Verification of Critical Systems. 〈inria-00540811〉

Partager

Métriques

Consultations de la notice

394

Téléchargements de fichiers

430