Description of the Chord Protocol using ASMs Formalism
Bojan Marinkovi\'c, Paola Glavan, Zoran Ognjanovi\'c
TL;DR
This paper formalizes the Chord protocol using Abstract State Machines to rigorously verify its correctness in maintaining ring topology and managing distributed keys.
Contribution
It introduces a formal ASM-based model of Chord, providing a rigorous correctness proof for its core actions and properties.
Findings
Formal ASM model of Chord developed
Correctness of Chord actions proven within the model
Provides a foundation for verifying distributed protocols
Abstract
This paper describes the overlay protocol Chord using the formalism of Abstract State Machines. The formalization concerns Chord actions that maintain ring topology and manipulate distributed keys. We define a class of runs and prove the correctness of our formalization with respect to it.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsPeer-to-Peer Network Technologies · Advanced Data Storage Technologies · Distributed systems and fault tolerance