| 一个分布式K互斥算法的概率模型检测 |
| |
| 引用本文： | 刘来,骆翔宇.一个分布式K互斥算法的概率模型检测[J].计算机应用研究,2015,32(4). |
| |
| 作者姓名： | 刘来 骆翔宇 |
| |
| 作者单位： | 1. 华侨大学计算机科学与技术学院,福建厦门,361021
2. 华侨大学计算机科学与技术学院,福建厦门361021;桂林电子科技大学广西可信软件重点实验室,广西桂林541004 |
| |
| 基金项目： | 国家自然科学基金面上项目，福建省高等学校新世纪优秀人才支持计划资助项目，华侨大学中青年教师科研提升计划资助项目，华侨大学高层次人才科研启动费项目，广西可信软件重点实验室研究项目 |
| |
| 摘 要： | 传统的验证方法难以保证分布式K互斥算法的有效性和安全性.为解决这一问题,给出了进一步的研究,提出一种基于概率模型检测器PRISM的方法,对Kerry Raymond的分布式K互斥算法进行形式化建模与分析验证.通过设置算法中各个进程进入临界区的时间而得出的结果中发现,改变临界区的数目K,对于某一进程进入临界区的平均及时时间的影响并不大.如果某一进程的执行时间比其他进程大很多,则K的增加可以提高运行效率.最后证明了这一结论.
|
| 关 键 词： | 分布式K互斥算法 概率模型检测 PRISM 平均及时时间 |
Probabilistic model checking for distributed K-mutual exclusion algorithm |
| |
| LIU Lai,LUO Xiang-yu.Probabilistic model checking for distributed K-mutual exclusion algorithm[J].Application Research of Computers,2015,32(4). |
| |
| Authors: | LIU Lai LUO Xiang-yu |
| |
| Abstract: | |
| |
| Keywords: | distributed K-mutual exclusion algorithm probabilistic model checking PRISM average timely time |
| 本文献已被 万方数据 等数据库收录！ |
|
