The State Space Analysis And Model Checking For A Class Of Round-Based Distributed Algorithms

With the rapid development of information technology, computer-based systems are widely used in our daily life, such as telecommunication systems, banking systems, etc. Most of these systems are critically dependent on their underlying distributed algorithms to achieve specific goals such as distributed agreement and fault tolerance. Clearly, it is important for the algorithms to run correctly and efficiently. Failures of these systems can be potentially disastrous. However, since the settings in which these algorithms operate are complicated, design of such algorithms is error-prone and can be an extremely difficult and complex task. The proper use of mathematical theory and analysis can enhance the validation and reliability of design. Model checking based formal verification is a technique of this kind, and has been successful used in practice to verify complex sequential circuit designs and communication protocols.Model checking verifies whether a desired property holds over a given system through an exhaustive exploration of all the states reachable by the system. When the number of global state space is very large or even infinite, the state space explosion problem would arise, and it is impossible to explore the entire state space of the system with limited resources of time and memory, thus makes the use of model checking infeasible. However, in the field of distributed computing, there exist many round-based algorithms to solve fundamental problems, such as leader election and distributed consensus. Since these problems have no deterministic solutions, these algorithms have to employee round numbers to achieve their goals with some probability. But this gives rise to the boundlessness of round numbers, and thus leads to the state space explosion problem when verifying correctness of these algorithms using model checking. Our goal is to model check these round-based distributed algorithms by means of dealing with the state space explosion problem.By investigating the inherent relations of round numbers, we find that although the round numbers may grow infinitely, the distance of round numbers is bounded by a finite value. In this thesis, we present a general idea, based on this observation, to model check these round-based algorithms. Instead of having an explicit representation of round numbers, we model round numbers by keeping their relative relations. Thus we are able to have a finite representation of round number, and then make (fully) automatic verification of these algorithms possible. Meanwhile, we also give a correctness proof for our approach.We apply this idea to two leader election algorithms (including a new proposed algorithm in the thesis) and two consensus algorithms. We list these four algorithms as well as the theoretical results we found as follows:1) The Itai-Rodeh leader election algorithm:for which we find that the distance of round numbers of active processes is at most 1; 2) A newly proposed leader election algorithm:for which the distance of round numbers of active processes is at most n-1; 3) A probabilistic consensus algorithm, which is proposed by Bracha and Toueg. We find that when only one process is allowed to crash, before some process decides the distance of round numbers of correct processes is at most 3; 4) A rotating coordinator algorithm with failure detector, for which we find that when only one process is allowed to crash, before some process decides, the distance of round numbers of correct processes is at most 2n.For each algorithm, we firstly investigate the inherent relations of round numbers and then give the result of their bounded distance with a correctness proof as well. Secondly, based on the result we found, we transform the state space of the algorithm into finite. And at last, we verify their correctness by using the model checker Spin.