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

Probabilistic model checking for distributed K-mutual exclusion algorithm

作　　者：刘来[1] 骆翔宇[1,2] 

机构地区：[1]华侨大学计算机科学与技术学院,福建厦门361021 [2]桂林电子科技大学广西可信软件重点实验室,广西桂林541004

出　　处：《计算机应用研究》2015年第4期1036-1039,共4页Application Research of Computers

基　　金：国家自然科学基金面上项目(61170028);福建省高等学校新世纪优秀人才支持计划资助项目(2013FJ-NCET-ZR03);华侨大学中青年教师科研提升计划资助项目(ZQN-YX109);华侨大学高层次人才科研启动费项目(11BS108);广西可信软件重点实验室研究项目(kx201323)

摘　　要：传统的验证方法难以保证分布式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.

关 键 词：分布式K互斥算法 概率模型检测 PRISM 平均及时时间 

分 类 号：TP301.6[自动化与计算机技术—计算机系统结构]