一个分布式K互斥算法的概率模型检测

Probabilistic model checking for distributed K-mutual exclusion algorithm

传统的验证方法难以保证分布式K互斥算法的有效性和安全性。为解决这一问题,给出了进一步的研究,提出一种基于概率模型检测器PRISM的方法,对Kerry Raymond的分布式K互斥算法进行形式化建模与分析验证。通过设置算法中各个进程进入临界区的时间而得出的结果中发现,改变临界区的数目K,对于某一进程进入临界区的平均及时时间的影响并不大。如果某一进程的执行时间比其他进程大很多,则K的增加可以提高运行效率。最后证明了这一结论。

It is hard for traditional experimental methods to guarantee the validity and safety of the distributed K-mutual exclusion algorithms. This paper resolved the problem,and gave more study. It proposed a formal verification and analysis method for a distributed K-mutual exclusion algorithm by Kerry Raymond,based on probabilistic model checker PRISM. According to set the time of processes entering critical region in the algorithm,it found that the change of the number K of critical regions had slight effect on the average timely time of one process to enter critical region. It further found that when the running time of one process was much longer than others,running efficiency of the algorithm could be improved by increasing the value of K. In addition,it proved the conclusion.