Verification And Analysis Of Distributed Algorithms Based On Probabilistic Model Checking

The value of distributed algorithms has important significance in practicalapplication. We propose a formal verification and analysis method for two classes ofdistributed algorithms, and prove the experiment of algorithm nature, based onprobabilistic model checking. Compared to the traditional methods, the technologycould be exhaustive state space, it makes the model more close to the realenvironment, then more conductive to validity and safety of researching algorithm byus; in addition, Markov method can analysis and verify uncertain factors in theprobabilistic model checker.The classes of algorithms for automatic recovery state in randomized distributedalgorithm, self-stabling algorithm. An algorithm resolves from faults in an N-processtoken ring by putting for a simple randomize solution by Mitchell Flatebo. He gives aconclusion for maximum stable time,0.5N2-0.5N-2, in the worst condition. But theprobability is very small. The expected worst time is important to our system inpractical application. We verify and analysis the algorithm by Flatebo, based onPRISM, and compared to another self-stabling algorithm by Ted Herman. With theincrease of number of nodes, we find that its performance is gradually improver thanHerman’s algorithm. Finally, we use linear regression to matching approximate valueof the expected worst time, and give a simple validation and analysis method ofself-stabling algorithms.The paper researches another distributed algorithm, randomized mutual exclusionalgorithm. It proposes a verification and analysis method for K-mutual exclusionalgorithm by Kerry Raymond, based on probabilistic model checking. We first verifytwo basic properties of mutual exclusion, no deadlock and no starvation. Then weverify the expected worst time for a process enter a critical region by PRISM; in theexperiment, we find that the change of the number K of critical regions has slighteffect on the average timely time of one or any process to enter critical region. Wefurther find that when the running time of one process is much longer than others, running efficiency of the algorithm can be improved by increasing the value of K.And we put forward a new k mutual exclusion by appending addition storagestructure. It cloud reduce number of sending and receiving messages for processes.Finally, it gives improved K distributed algorithm...