《计算机应用研究》|Application Research of Computers

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

Probabilistic model checking for distributed K-mutual exclusion algorithm

免费全文下载 (已被下载 次)  
获取PDF全文
作者 刘来,骆翔宇
机构 1.华侨大学 计算机科学与技术学院,福建 厦门 361021;2.桂林电子科技大学 广西可信软件重点实验室,广西 桂林 541004
统计 摘要被查看 次,已被下载
文章编号 1001-3695(2015)04-1036-04
DOI 10.3969/j.issn.1001-3695.2015.04.018
摘要 传统的验证方法难以保证分布式K互斥算法的有效性和安全性。为解决这一问题,给出了进一步的研究,提出一种基于概率模型检测器PRISM的方法,对Kerry Raymond的分布式K互斥算法进行形式化建模与分析验证。通过设置算法中各个进程进入临界区的时间而得出的结果中发现,改变临界区的数目K,对于某一进程进入临界区的平均及时时间的影响并不大。如果某一进程的执行时间比其他进程大很多,则K的增加可以提高运行效率。最后证明了这一结论。
关键词 分布式K互斥算法;概率模型检测;PRISM;平均及时时间
基金项目 国家自然科学基金面上项目(61170028)
福建省高等学校新世纪优秀人才支持计划资助项目(2013FJ-NCET-ZR03)
华侨大学中青年教师科研提升计划资助项目(ZQN-YX109)
华侨大学高层次人才科研启动费项目(11BS108)
广西可信软件重点实验室研究项目(kx201323)
本文URL http://www.arocmag.com/article/01-2015-04-018.html
英文标题 Probabilistic model checking for distributed K-mutual exclusion algorithm
作者英文名 LIU Lai, LUO Xiang-yu
机构英文名 1. College of Computer Science & Technology, Huaqiao University, Xiamen Fujian 361021, China; 2. Guangxi Key Laboratory of Trusted Software, Guilin University of Electronic Technology, Guilin Guangxi 541004, China
英文摘要 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.
英文关键词 distributed K-mutual exclusion algorithm; probabilistic model checking; PRISM; average timely time
参考文献 查看稿件参考文献
  [1] RICART G, AGRAWALA A K. An optimal algorithm for mutual exclusion in computer networks[J] . Communications of the ACM, 1981, 24(1):9-17.
[2] RAYMOND K. A distributed algorithm for multiple entries to a critical section[J] . Information Processing Letters, 1989, 30(4):189-193.
[3] MATEESCU R, SERWE W. Model checking and performance evalua-tion with CADP illustrated on shared-memory mutual exclusion protocols[J] . Science of Computer Programming, 2013, 78(7):843-861.
[4] KATZ G, PELED D. Model checking-based genetic programming with an application to mutual exclusion:proceedings of the Theory and practice of software[C] //Proc of the 14th International Confe-rence on Tools and Algorithms for the Construction and Analysis of Systems. Berlin:Springer-Verlag, 2008:141-156.
[5] KATZ G, PELED D. Genetic programming and model checking:synthesizing new mutual exclusion algorithms[C] //Proc of the 6th International Symposium on Automated Technology for Verification and Analysis. Berlin:Springer-Verlag, 2008:33-47.
[6] HINTON A, KWIATKOWSKA M, NORMAN G, et al. PRISM:a tool for automatic verification of probabilistic systems[C] //Proc of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin:Springer, 2006:441-444.
[7] KWIATKOWSKA M, NORMAN G, PARKER D. PRISM:probabilistic symbolic model checker[C] //Proc of the 12th International Conference on Computer Performance Evaluation, Modelling Techniques and Tools. London:Springer-Verlag, 2002:200-204.
[8] BULGANNAWAR S, VAIDYA N F. A distributed K-mutual exclusion algorithm[C] //Proc of the 15th International Conference on Distributed Computing Systems. Washington DC:IEEE Computer Society, 1995:153-160.
[9] TREHEL M, NAIMI M. A distributed algorithm for mutual exclusion based on data structures and fault tolerance[C] //Proc of the 6th Annual International Phoenix Conference on Computers and Communications. 1987:35-39.
收稿日期 2014/3/3
修回日期 2014/5/15
页码 1036-1039
中图分类号 TP301.6
文献标志码 A