Correctness of the Chord Protocol

Bojan Marinković¹, Zoran Ognjanović¹, Paola Glavan², Anton Kos³ and Anton Umek³

Mathematical Institute of the Serbian Academy of Sciences and Arts
Beograd, Serbia
{bojanm,zorano}@mi.sanu.ac.rs
Faculty of Mechanical Engineering and Naval Architecture
University of Zagreb, Zagreb, Croatia
pglavan@fsb.hr
Faculty of Electrical Engineering
University of Ljubljana, Ljubljana, Slovenia
{anton.kos, anton.umek}@fe.uni-lj.si

Abstract

Internet of Things (IoT) can be seen as a cooperation of various devices with limited performances that participate in the same system. IoT devices compose a distributed architecture system. The core of every IoT system is its discovery and control services. To realize such services, some authors used the developed solutions from the different domains. One such solution is the Chord protocol, one of the first, the simplest and the most popular distributed protocols. Unfortunately, the application of the Chord protocol was realized using the correctness of the Chord protocol for granted, or by the very hard assumptions. In this paper we prove the correctness of the Chord protocol using the logic of time and knowledge with the respect to the set of possible executions, called regular runs. We provide the deterministic description of the correctness of the Chord protocol and consider Chord actions that maintain ring topology while the nodes can freely join or leave.

Key words

IoT, DHT, Chord, correctness, temporal logic, epistemic logic

Digital Object Identifier (DOI)

https://doi.org/10.2298/CSIS181115017M

Publication information

Volume 17, Issue 1 (January 2020)
Year of Publication: 2020
ISSN: 2406-1018 (Online)
Publisher: ComSIS Consortium

Full text

Download Available in PDF
Portable Document Format

How to cite

Marinković, B., Ognjanović, Z., Glavan, P., Kos, A., Umek, A.: Correctness of the Chord Protocol. Computer Science and Information Systems, Vol. 17, No. 1, 141-160. (2020), https://doi.org/10.2298/CSIS181115017M