Towards Verification of the Pastry Protocol using TLA+
Identifieur interne : 004E47 ( Hal/Curation ); précédent : 004E46; suivant : 004E48Towards Verification of the Pastry Protocol using TLA+
Auteurs : Stephan Merz [France] ; Tianxiang Lu [Allemagne] ; Christoph Weidenbach [Allemagne]Source :
English descriptors
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.
Url:
Links toward previous steps (curation, corpus...)
- to stream Hal, to step Corpus: Pour aller vers cette notice dans l'étape Curation :004E47
Links to Exploration step
Hal:inria-00593523Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">Towards Verification of the Pastry Protocol using TLA+</title><author><name sortKey="Merz, Stephan" sort="Merz, Stephan" uniqKey="Merz S" first="Stephan" last="Merz">Stephan Merz</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-107895" status="VALID"><idno type="RNSR">201020692C</idno><orgName>Modeling and Verification of Distributed Algorithms and Systems</orgName><orgName type="acronym">VERIDIS</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/veridis</ref></desc><listRelation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-129671" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno><idno type="ISNI">0000000122597504</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><settlement type="city">Metz</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université de Lorraine</orgName></affiliation></author><author><name sortKey="Lu, Tianxiang" sort="Lu, Tianxiang" uniqKey="Lu T" first="Tianxiang" last="Lu">Tianxiang Lu</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-54489" status="VALID"><orgName>Max Planck Institut für Informatik</orgName><orgName type="acronym">MPII</orgName><desc><address><addrLine>Max Planck Institut für Informatik Campus E-1 4 66123 Saarbrücken Germany</addrLine><country key="DE"></country></address><ref type="url">http://www.mpi-inf.mpg.de/</ref></desc><listRelation><relation active="#struct-300044" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300044" type="direct"><org type="institution" xml:id="struct-300044" status="VALID"><orgName>Max-Planck-Institut</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Allemagne</country><orgName type="university">Société Max-Planck</orgName></affiliation></author><author><name sortKey="Weidenbach, Christoph" sort="Weidenbach, Christoph" uniqKey="Weidenbach C" first="Christoph" last="Weidenbach">Christoph Weidenbach</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-54489" status="VALID"><orgName>Max Planck Institut für Informatik</orgName><orgName type="acronym">MPII</orgName><desc><address><addrLine>Max Planck Institut für Informatik Campus E-1 4 66123 Saarbrücken Germany</addrLine><country key="DE"></country></address><ref type="url">http://www.mpi-inf.mpg.de/</ref></desc><listRelation><relation active="#struct-300044" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300044" type="direct"><org type="institution" xml:id="struct-300044" status="VALID"><orgName>Max-Planck-Institut</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Allemagne</country><orgName type="university">Société Max-Planck</orgName></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:inria-00593523</idno><idno type="halId">inria-00593523</idno><idno type="halUri">https://hal.inria.fr/inria-00593523</idno><idno type="url">https://hal.inria.fr/inria-00593523</idno><date when="2011-06">2011-06</date><idno type="wicri:Area/Hal/Corpus">004E47</idno><idno type="wicri:Area/Hal/Curation">004E47</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Towards Verification of the Pastry Protocol using TLA+</title><author><name sortKey="Merz, Stephan" sort="Merz, Stephan" uniqKey="Merz S" first="Stephan" last="Merz">Stephan Merz</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-107895" status="VALID"><idno type="RNSR">201020692C</idno><orgName>Modeling and Verification of Distributed Algorithms and Systems</orgName><orgName type="acronym">VERIDIS</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/veridis</ref></desc><listRelation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-129671" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno><idno type="ISNI">0000000122597504</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><settlement type="city">Metz</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université de Lorraine</orgName></affiliation></author><author><name sortKey="Lu, Tianxiang" sort="Lu, Tianxiang" uniqKey="Lu T" first="Tianxiang" last="Lu">Tianxiang Lu</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-54489" status="VALID"><orgName>Max Planck Institut für Informatik</orgName><orgName type="acronym">MPII</orgName><desc><address><addrLine>Max Planck Institut für Informatik Campus E-1 4 66123 Saarbrücken Germany</addrLine><country key="DE"></country></address><ref type="url">http://www.mpi-inf.mpg.de/</ref></desc><listRelation><relation active="#struct-300044" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300044" type="direct"><org type="institution" xml:id="struct-300044" status="VALID"><orgName>Max-Planck-Institut</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Allemagne</country><orgName type="university">Société Max-Planck</orgName></affiliation></author><author><name sortKey="Weidenbach, Christoph" sort="Weidenbach, Christoph" uniqKey="Weidenbach C" first="Christoph" last="Weidenbach">Christoph Weidenbach</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-54489" status="VALID"><orgName>Max Planck Institut für Informatik</orgName><orgName type="acronym">MPII</orgName><desc><address><addrLine>Max Planck Institut für Informatik Campus E-1 4 66123 Saarbrücken Germany</addrLine><country key="DE"></country></address><ref type="url">http://www.mpi-inf.mpg.de/</ref></desc><listRelation><relation active="#struct-300044" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300044" type="direct"><org type="institution" xml:id="struct-300044" status="VALID"><orgName>Max-Planck-Institut</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Allemagne</country><orgName type="university">Société Max-Planck</orgName></affiliation></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="mix" xml:lang="en"><term>formal specification</term><term>model checking</term><term>network protocols</term><term>verification methods</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">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.</div></front></TEI><hal api="V3"><titleStmt><title xml:lang="en">Towards Verification of the Pastry Protocol using TLA+</title><author role="aut"><persName><forename type="first">Stephan</forename><surname>Merz</surname></persName><email>Stephan.Merz@loria.fr</email><idno type="halauthor">66750</idno><affiliation ref="#struct-107895"></affiliation><affiliation ref="#struct-140234"></affiliation><affiliation ref="#struct-65197"></affiliation></author><author role="aut"><persName><forename type="first">Tianxiang</forename><surname>Lu</surname></persName><email></email><idno type="halauthor">552270</idno><orgName ref="#struct-300044"></orgName><affiliation ref="#struct-54489"></affiliation></author><author role="aut"><persName><forename type="first">Christoph</forename><surname>Weidenbach</surname></persName><email></email><idno type="halauthor">129856</idno><orgName ref="#struct-364522"></orgName><affiliation ref="#struct-54489"></affiliation></author><editor role="depositor"><persName><forename>Stephan</forename><surname>Merz</surname></persName><email>Stephan.Merz@loria.fr</email></editor></titleStmt><editionStmt><edition n="v1" type="current"><date type="whenSubmitted">2011-05-16 14:00:18</date><date type="whenModified">2015-09-22 01:12:10</date><date type="whenReleased">2011-05-16 14:00:18</date><date type="whenProduced">2011-06</date></edition><respStmt><resp>contributor</resp><name key="104076"><persName><forename>Stephan</forename><surname>Merz</surname></persName><email>Stephan.Merz@loria.fr</email></name></respStmt></editionStmt><publicationStmt><distributor>CCSD</distributor><idno type="halId">inria-00593523</idno><idno type="halUri">https://hal.inria.fr/inria-00593523</idno><idno type="halBibtex">merz:inria-00593523</idno><idno type="halRefHtml">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</idno><idno type="halRef">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</idno></publicationStmt><seriesStmt><idno type="stamp" n="INRIA">INRIA - Institut National de Recherche en Informatique et en Automatique</idno><idno type="stamp" n="INRIA-NANCY-GRAND-EST">INRIA Nancy - Grand Est</idno><idno type="stamp" n="CNRS">CNRS - Centre national de la recherche scientifique</idno><idno type="stamp" n="UNIV-NANCY1">Université Henri Poincaré - Nancy I</idno><idno type="stamp" n="UNIV-NANCY2">Université Nancy II</idno><idno type="stamp" n="LABO-LORIA-SET" p="LORIA">LABO-LORIA-SET</idno><idno type="stamp" n="LORIA-FM" p="LORIA">Méthodes formelles</idno><idno type="stamp" n="INRIA-LORRAINE">INRIA Nancy - Grand Est</idno><idno type="stamp" n="LORIA">LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications</idno><idno type="stamp" n="LORIA2">Publications du LORIA</idno><idno type="stamp" n="UNIV-LORRAINE">Université de Lorraine</idno><idno type="stamp" n="INPL">Institut National Polytechnique de Lorraine</idno><idno type="stamp" n="INRIA_TEST">INRIA - Institut National de Recherche en Informatique et en Automatique</idno></seriesStmt><notesStmt><note type="audience" n="2">International</note><note type="invited" n="0">No</note><note type="popular" n="0">No</note><note type="peer" n="1">Yes</note><note type="proceedings" n="1">Yes</note></notesStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Towards Verification of the Pastry Protocol using TLA+</title><author role="aut"><persName><forename type="first">Stephan</forename><surname>Merz</surname></persName><email>Stephan.Merz@loria.fr</email><idno type="halAuthorId">66750</idno><affiliation ref="#struct-107895"></affiliation><affiliation ref="#struct-140234"></affiliation><affiliation ref="#struct-65197"></affiliation></author><author role="aut"><persName><forename type="first">Tianxiang</forename><surname>Lu</surname></persName><idno type="halAuthorId">552270</idno><orgName ref="#struct-300044"></orgName><affiliation ref="#struct-54489"></affiliation></author><author role="aut"><persName><forename type="first">Christoph</forename><surname>Weidenbach</surname></persName><idno type="halAuthorId">129856</idno><orgName ref="#struct-364522"></orgName><affiliation ref="#struct-54489"></affiliation></author></analytic><monogr><meeting><title>31st IFIP International Conference on Formal Techniques for Networked and Distributed Systems</title><date type="start">2011-06</date><settlement>Reykjavik</settlement><country key="IS">Iceland</country></meeting><editor>R. Bruni and J. Dingel</editor><imprint><biblScope unit="serie">FMOODS/FORTE 2011</biblScope><biblScope unit="volume">6722</biblScope><date type="datePub">2011-06</date></imprint></monogr></biblStruct></sourceDesc><profileDesc><langUsage><language ident="en">English</language></langUsage><textClass><keywords scheme="author"><term xml:lang="en">formal specification</term><term xml:lang="en">model checking</term><term xml:lang="en">verification methods</term><term xml:lang="en">network protocols</term></keywords><classCode scheme="acm" n="D.2.4.2"></classCode><classCode scheme="acm" n="D.2.4.3"></classCode><classCode scheme="acm" n="C.2.4"></classCode><classCode scheme="halDomain" n="info.info-lo">Computer Science [cs]/Logic in Computer Science [cs.LO]</classCode><classCode scheme="halTypology" n="COMM">Conference papers</classCode></textClass><abstract xml:lang="en">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.</abstract></profileDesc></hal></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Hal/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 004E47 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Hal/Curation/biblio.hfd -nk 004E47 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Hal
|étape= Curation
|type= RBID
|clé= Hal:inria-00593523
|texte= Towards Verification of the Pastry Protocol using TLA+
}}
| This area was generated with Dilib version V0.6.33. |  |