Authors: Marinković, Bojan 
Ognjanović, Zoran 
Glavan, Paola
Kos, Anton
Umek, Anton
Affiliations: Mathematical Institute of the Serbian Academy of Sciences and Arts 
Title: Correctness of the chord protocol
Journal: Computer Science and Information Systems
Volume: 17
Issue: 1
First page: 141
Last page: 160
Issue Date: 1-Jan-2020
Rank: M23
ISSN: 1820-0214
DOI: 10.2298/CSIS181115017M
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.
Keywords: Chord | Correctness | DHT | Epistemic logic | IoT | Temporal logic
Publisher: ComSIS Consortium
Project: Representations of logical structures and formal languages and their application in computing 
Development of new information and communication technologies, based on advanced mathematical methods, with applications in medicine, telecommunications, power systems, protection of national heritage and education 

Show full item record

Page view(s)

checked on Aug 15, 2022

Google ScholarTM




Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.