Framework for Exploration, Development and Testing of the Distributed Algorithms in the Presence of Faults

This thesis will describe the main challenging problem in development of distributed algorithms which is the testing them in the presence of faults and verifying correctness of a specific implementations of specific algorithm. There are two classes of approaches to verify correctness of a distributed algorithm. The first one consists of the techniques that use formal methods that provide a machinery to automatically prove the correctness of an algorithm based on its formal specification. The second one includes the framework that provide an API to emulate the work of a distributed application in a specific scenario. Existing solutions of each classes of approaches are observed in the corresponding part of the thesis, and a proposed framework is described as a result of the thesis. As an example Lamport’s mutex algorithm was implemented and tested. Keywords: Distributed Systems, Distributed Algorithms, Fault-Tolerance, Testing