Proving properties of the Chord protocol using the ASM formalism

DOI10.1016/J.TCS.2018.10.025MaRDI QIDQ1757159zbMATH OpenOpenAlexWikidataFDO

Authors Bojan Marinković, Paola Glavan, Zoran Ognjanović

Publication date 2 January 2019

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2018.10.025

zbMATH Keywords

abstract state machinespeer-to-peerChordformal descriptionDHT-based overlay networks

Mathematics Subject Classification ID

Network design and communication in computer systems (68M10) Distributed systems (68M14) Network protocols (68M12)

Recommendations

• Global Computing
• Formal verification of Multi-Paxos for distributed consensus
• The DHCP Failover Protocol: A Formal Perspective
• Specifying and Analyzing the Kademlia Protocol in Maude
• Formal modeling and analysis of a narrow bandwidth protocol for establishing and terminating connections

Cites work

• scientific article; zbMATH DE number 1543079 (Why is no real title available?)
• scientific article; zbMATH DE number 1559581 (Why is no real title available?)
• scientific article; zbMATH DE number 2172808 (Why is no real title available?)
• scientific article; zbMATH DE number 868108 (Why is no real title available?)
• Abstract State Machines
• Analysis of the evolution of peer-to-peer systems
• Can abstract state machines be useful in language theory?
• Evolving Algebras 1993: Lipari Guide
• From P2P to web services and grids. Peers in a client/server world.
• Sequential abstract-state machines capture sequential algorithms

Cited in

(4)

• The DHCP Failover Protocol: A Formal Perspective
• Formal modeling and analysis of a narrow bandwidth protocol for establishing and terminating connections
• Global Computing
• Mechanically verifying the fundamental liveness property of the Chord protocol

Describes a project that uses

Uses Software

• Bigtable
• Cassandra
• Chord

This page was built for publication: Proving properties of the Chord protocol using the ASM formalism

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1757159)