Construction and Formal Verification of a Fault-Tolerant Distributed Mutual Exclusion Algorithm

Distributed fault-tolerant control algorithms are in great demand nowadays due to their practical importance in cloud computing, Internet of Things (IoT) technology, swarm robotics, and other areas. It is usually hard to make a distributed algorithm fault-tolerant. It is even harder to ensure that such algorithm behaves correctly in the presence of faults of some kind. In this work, we construct a reliable, adaptive, fault-tolerant distributed mutual exclusion algorithm based on the well-known Ricart-Agrawala algorithm. In order to formally verify it, we use a hybrid approach of deductive reasoning and bounded model-checking. First, a safety property of the Ricart-Agrawala algorithm is proved in Calculus of Inductive Constructions of Coq proof assistant using assertional reasoning. Then, an extension of that algorithm turning it into fault-tolerant and adaptive to participants set change, is formalized in TLA and checked on a bounded model. Besides constructing and verifying the algorithm, this work aims to familiarize those interested in constructing highly reliable components with well established verification methods that were used to verify the proposed algorithm.