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

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