基于概率模型检测的动态系统领导者选举协议分析与验证

发布时间：2017-08-03 02:24

  本文关键词：基于概率模型检测的动态系统领导者选举协议分析与验证

  更多相关文章： 形式化验证 概率模型检测 领导者选举协议 动态系统

【摘要】：领导者选举协议是分布式计算中的重要协议。它能够保证分布式系统选举出唯一的领导者,使之协同系统中其余进程的工作,以此提高整个系统的工作效率。随着动态系统逐渐成为分布式计算的研究热点,在该系统中的领导者选举协议的设计和验证获得较多的关注。对于该协议的验证,必须立足于动态系统。由于动态系统中包含了很多不确定的因素,这给传统的基于模型检测的协议验证方法带来了很大的挑战。本文采用概率模型检测技术,对这种广泛存在的不确定性进行建模,围绕着动态系统中的领导者选举协议进行了较为系统的分析,并应用主流开源概率模型检测工具PRISM对最近提出的层次式领导者选举协议进行建模与验证。(1)在模型分析的过程中,针对模型检测领域常见的“状态爆炸”问题,本文通过简化协议的内部操作,删除多余步骤,来减少模型的状态数。对其中不确定的行为,通过为其设定概率系数,取代原先复杂的条件判定操作,从而缓解了模型状态爆炸问题的产生。(2)在模型构建的过程中,引入了“假设-保证”的组合式验证思想,将层次式协议进行分别处理,建立了一个具有双层结构的领导者选举协议模型,并通过实验,给出了具体验证结果,显示了该模型的有效性。(3)在整个实验的过程中,针对模型中含有大量相似的内容造成代码重复书写的问题,本文提出了一种自动生成PRISM代码的方法,在很大程度上提高了代码的编写效率。并且借助于C语言,完成了简易的PRISM代码自动生成的脚本程序。本文的研究意义在于对近期提出的层次式领导者选举协议进行了分层建模与验证,验证模型的规模和效率比传统的整体式验证都有了很大的提升,为动态系统中领导者的确定,提供了一种比较合理的方法,增强了动态系统的工作效率。
【关键词】：形式化验证 概率模型检测 领导者选举协议 动态系统
【学位授予单位】：南京航空航天大学
【学位级别】：硕士
【学位授予年份】：2016
【分类号】：TP338.8
【目录】：

• 摘要4-5
• ABSTRACT5-10
• 注释表10-11
• 缩略词11-12
• 第一章 绪论12-17
• 1.1 研究背景和意义12-13
• 1.2 研究现状13-15
• 1.3 主要研究内容15-16
• 1.4 文章的组织结构16-17
• 第二章 相关概念和工具介绍17-21
• 2.1 相关概念17-19
• 2.1.1 概率模型检测17-18
• 2.1.2 动态系统18
• 2.1.3 领导者选举协议18-19
• 2.2 PRISM简介19
• 2.3 本章小结19-21
• 第三章 动态系统层次式领导者选举协议的介绍21-36
• 3.1 系统模型与假设21-24
• 3.1.1 进程与簇21-22
• 3.1.2 异步性与稳定性22-23
• 3.1.3“询问-回复”操作与相关假设23-24
• 3.2 动态系统领导者选举协议介绍24-35
• 3.2.1 下层领导者选举协议24-31
• 3.2.2 上层领导者选举协议31-35
• 3.3 本章小结35-36
• 第四章 构建PRISM概率模型36-49
• 4.1 相关理论支持36-37
• 4.1.1 假设-保证验证36
• 4.1.2 布尔型变量法实现集合交、并操作36-37
• 4.2 下层领导者选举模型的构建和属性验证37-42
• 4.2.1 流程状态分析38
• 4.2.2 协议-模型转化38-42
• 4.3 上层领导者选举模型的构建和属性验证42-45
• 4.3.1 流程状态分析43
• 4.3.2 协议-模型转化43-45
• 4.4 基于C语言的自动生成建模脚本语言45-48
• 4.4.1 参数化分析46-47
• 4.4.2 区域化实现47-48
• 4.5 本章小结48-49
• 第五章 关于协议可靠性的PRISM模型验证49-62
• 5.1 基于假设-保证的分层建模可靠性验证49-55
• 5.1.1 下层模型属性验证49-52
• 5.1.2 上层模型属性验证52-55
• 5.2 模型分层与整体验证开销对比55-58
• 5.2.1 模型分层验证的开销55-56
• 5.2.2 模型整体验证的开销56-58
• 5.3 不稳定环境下领导者选举协议的可靠性分析58-60
• 5.3.1 下层环境不稳定对协议可靠性的影响58-59
• 5.3.2 上层环境不稳定对协议可靠性的影响59-60
• 5.4 本章小结60-62
• 第六章 总结与展望62-63
• 参考文献63-67
• 致谢67-68
• 在学期间的研究成果及发表的学术论文68

【参考文献】

中国期刊全文数据库 前10条

1 马银雪;陈哲;黄志球;黄吴丹;;使用模型检验自动化验证路由协议[J];小型微型计算机系统;2015年11期

2 周筱羽;顾斌;赵建华;杨孟飞;李宣东;;中断驱动系统模型检验?[J];软件学报;2015年09期

3 张伟伟;宋晓琳;张三林;吴训成;;基于软硬件协同设计的车道线实时识别方法[J];中国机械工程;2015年10期

4 夏春蕊;王瑞;李晓娟;关永;;概率模型检测技术在机器人路径规划中的应用[J];计算机仿真;2015年03期

5 刘来;骆翔宇;;一个分布式K互斥算法的概率模型检测[J];计算机应用研究;2015年04期

6 支志兵;;容斥原理在汉密尔顿问题中的应用[J];数学理论与应用;2014年02期

7 庄t-;沈昌祥;蔡勉;;基于行为的可信动态度量的状态空间约简研究[J];计算机学报;2014年05期

8 贾宁;杨春;佟冬;王克义;;动态翻译系统中的间接转移关联软件预测算法[J];计算机研究与发展;2014年03期

9 周东华;史建涛;何潇;;动态系统间歇故障诊断技术综述[J];自动化学报;2014年02期

10 田浪军;陈卫卫;陈卫东;李涛;;云存储系统中动态负载均衡算法研究[J];计算机工程;2013年10期

中国博士学位论文全文数据库 前1条

1 刘志锋;模型检测中关键技术的研究及其应用[D];南京大学;2011年

中国硕士学位论文全文数据库 前2条

1 陈道喜;基于Promela的组合抽象Spin模型检测及应用[D];苏州大学;2009年

2 王敏飞;模型检测在安全协议验证中的研究与应用[D];南京航空航天大学;2009年

，

本文编号：612284