Analyzing And Verification Of Leader Election Protocol In Dynamic Systems Via Probabilistic Model Checking

Leader election protocol is one of important protocols in distributed computing. It can guarantee a unique leader of the distributed system to be elected for sake of coordinating other processes and thus improve the productivity of the whole system. With the increasing development of the dynamic system which has gradually become a hot topic in distributed system, leader election protocols in such context have attracted more and more attention.Since the inherent uncertain traits of the dynamic systems, the traditional approaches of model checking are full of great challenges. According to the leader election protocol in the dynamic systems, this paper adopts the probabilistic model checking to build the model and verify some specific properties and utilizes the mainstream and open-source probabilistic model checking tool PRISM to model and verify the hierarchy-based leader election protocol proposed recently.(1) During the period of model analyzing, this paper abstracts the model behaviors to simplify some inner operations and delete some redundant steps to reduce the number of states of the model in order to mitigate the ‘state explosion' problem. Besides, some probabilities as parameters have been used simultaneously to replace some guards.(2) During the period of model construction, this thesis employs the concept of assume-guarantee technique to tackle the hierarchical protocol verification more efficiently and set up a two-layer leader election model.(3) During the process of experiment, for sake of solving the problem of repeatedly writing the code with various components with similar structures, this paper proposes an efficient approach to automatically generate the PRISM code implemented in C programming language to make the code parameterized in order to enhance the efficiency of coding.The significance of this paper is to layer by layer build and verify a hierarchy-based leader election protocol proposed recently and this method leads to enlarge the scale of the model and improve the efficiency of verification comparing it with the traditional integral verification. It provides a rational method of determining a leader in the dynamic system and then enhances the productivity of a dynamic system.