Towards Verification of the Pastry Protocol Using TLA +
International audience 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 pro...
Main Authors: | , , |
---|---|
Other Authors: | , , , , , , , , , |
Format: | Conference Object |
Language: | English |
Published: |
HAL CCSD
2011
|
Subjects: | |
Online Access: | https://inria.hal.science/hal-01583322 https://inria.hal.science/hal-01583322/document https://inria.hal.science/hal-01583322/file/978-3-642-21461-5_16_Chapter.pdf https://doi.org/10.1007/978-3-642-21461-5_16 |
id |
ftunilorrainehal:oai:HAL:hal-01583322v1 |
---|---|
record_format |
openpolar |
spelling |
ftunilorrainehal:oai:HAL:hal-01583322v1 2023-10-09T21:52:45+02:00 Towards Verification of the Pastry Protocol Using TLA + Lu, Tianxiang Merz, Stephan Weidenbach, Christoph Max-Planck-Institut für Informatik (MPII) Max-Planck-Gesellschaft VERIfication pour les systèmes DIStribués (VERIDIS) Inria Nancy - Grand Est Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA) Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS) Roberto Bruni Juergen Dingel TC 6 WG 6.1 Reykjavik, Iceland 2011-06-06 https://inria.hal.science/hal-01583322 https://inria.hal.science/hal-01583322/document https://inria.hal.science/hal-01583322/file/978-3-642-21461-5_16_Chapter.pdf https://doi.org/10.1007/978-3-642-21461-5_16 en eng HAL CCSD Springer info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-642-21461-5_16 hal-01583322 https://inria.hal.science/hal-01583322 https://inria.hal.science/hal-01583322/document https://inria.hal.science/hal-01583322/file/978-3-642-21461-5_16_Chapter.pdf doi:10.1007/978-3-642-21461-5_16 http://creativecommons.org/licenses/by/ info:eu-repo/semantics/OpenAccess Lecture Notes in Computer Science 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE) https://inria.hal.science/hal-01583322 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik, Iceland. pp.244-258, ⟨10.1007/978-3-642-21461-5_16⟩ network protocols verification methods model checking formal specification [INFO]Computer Science [cs] [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI] info:eu-repo/semantics/conferenceObject Conference papers 2011 ftunilorrainehal https://doi.org/10.1007/978-3-642-21461-5_16 2023-09-12T23:25:41Z International audience 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. Conference Object Iceland Université de Lorraine: HAL 244 258 |
institution |
Open Polar |
collection |
Université de Lorraine: HAL |
op_collection_id |
ftunilorrainehal |
language |
English |
topic |
network protocols verification methods model checking formal specification [INFO]Computer Science [cs] [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI] |
spellingShingle |
network protocols verification methods model checking formal specification [INFO]Computer Science [cs] [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI] Lu, Tianxiang Merz, Stephan Weidenbach, Christoph Towards Verification of the Pastry Protocol Using TLA + |
topic_facet |
network protocols verification methods model checking formal specification [INFO]Computer Science [cs] [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI] |
description |
International audience 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. |
author2 |
Max-Planck-Institut für Informatik (MPII) Max-Planck-Gesellschaft VERIfication pour les systèmes DIStribués (VERIDIS) Inria Nancy - Grand Est Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA) Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS) Roberto Bruni Juergen Dingel TC 6 WG 6.1 |
format |
Conference Object |
author |
Lu, Tianxiang Merz, Stephan Weidenbach, Christoph |
author_facet |
Lu, Tianxiang Merz, Stephan Weidenbach, Christoph |
author_sort |
Lu, Tianxiang |
title |
Towards Verification of the Pastry Protocol Using TLA + |
title_short |
Towards Verification of the Pastry Protocol Using TLA + |
title_full |
Towards Verification of the Pastry Protocol Using TLA + |
title_fullStr |
Towards Verification of the Pastry Protocol Using TLA + |
title_full_unstemmed |
Towards Verification of the Pastry Protocol Using TLA + |
title_sort |
towards verification of the pastry protocol using tla + |
publisher |
HAL CCSD |
publishDate |
2011 |
url |
https://inria.hal.science/hal-01583322 https://inria.hal.science/hal-01583322/document https://inria.hal.science/hal-01583322/file/978-3-642-21461-5_16_Chapter.pdf https://doi.org/10.1007/978-3-642-21461-5_16 |
op_coverage |
Reykjavik, Iceland |
genre |
Iceland |
genre_facet |
Iceland |
op_source |
Lecture Notes in Computer Science 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE) https://inria.hal.science/hal-01583322 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik, Iceland. pp.244-258, ⟨10.1007/978-3-642-21461-5_16⟩ |
op_relation |
info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-642-21461-5_16 hal-01583322 https://inria.hal.science/hal-01583322 https://inria.hal.science/hal-01583322/document https://inria.hal.science/hal-01583322/file/978-3-642-21461-5_16_Chapter.pdf doi:10.1007/978-3-642-21461-5_16 |
op_rights |
http://creativecommons.org/licenses/by/ info:eu-repo/semantics/OpenAccess |
op_doi |
https://doi.org/10.1007/978-3-642-21461-5_16 |
container_start_page |
244 |
op_container_end_page |
258 |
_version_ |
1779315929185779712 |