Correctness of the Chord Protocol

TL;DR

This paper formally proves the correctness of the Chord protocol, a fundamental distributed system protocol used in IoT networks, under the assumption of no node failures or departures.

Contribution

It provides a formal correctness proof of Chord using temporal and epistemic logic, enhancing understanding of its reliability in IoT applications.

Findings

Chord maintains ring topology under specified conditions

Correctness is proven using logic of time and knowledge

Assumes no node failures or departures

Abstract

Internet of Things (IoT) can be seen as a cooperation of the various heterogeneous devices with limited performances, that participate in the same system. By they nature, these devices can be very distributed. The core of every IoT system is its discovery and control service. The Chord protocol is one of the first, simplest and most popular distributed protocol and can be use as a backbone of the discovery and control services of an IoT system. In this paper we prove the correctness of the Chord protocol using the logic of time and knowledge. We consider Chord actions that maintain ring topology with the additional assumption the nodes are not allowed to fail or leave.