engleski

Proving properties of the Chord protocol using the ASM formalism

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-to-peer ; chord ; DHT-based overlay networks ; abstract state machines

nije evidentirano