并发系统中基于偏序规约的状态空间约简与应用

发布时间：2017-10-12 01:47

  本文关键词：并发系统中基于偏序规约的状态空间约简与应用

  更多相关文章： 模型检测 偏序规约 顽固集 领导选举

【摘要】：随着人们对软硬件系统功能需求的日益增加,导致系统的规模越来越复杂,其安全性和可靠性也越来越难以得到保证。在一些关键领域,例如航空航天、银行、证券等,软件可靠性问题显得尤为重要,已经日益成为当今研究的重要课题。在过去的三十几年间,针对并发系统运行的不确定性,各国研究人员为解决可靠性问题做出了许多工作,其中,模型检测验证技术就是该领域中的热点之一。模型检测是一种形式化自动验证技术,它可以为许多软件设计中的相关问题提出解决办法。一般给定一个系统的形式化数学模型以及形式化的规约属性,就可以使用模型检测技术验证该系统是否满足属性。自动检测器的检测结果要不证明该系统满足该属性,要不提供一个反例路径。然而,对于许多类型的系统来说,随着建模系统规模和进程数目的扩大,运行过程中可能产生的状态数将呈指数级增长,这就引起了状态爆炸问题。偏序规约技术就是为了缓解异步并发系统的状态爆炸问题而产生的,该技术主要是构建一个更小的状态空间子集,而搜索时仅探测该状态空间子集,并不是探测所有的并发交错运行。本文中,我们对模型检测技术和偏序规约技术进行深入的研究,主要工作如下:1、详述了并发系统的形式化描述方法及模型检测的一些基本原则,并研究如何使用TLA+语言对现实问题进行规约。2、研究了偏序规约的相关理论,同时对几种约简状态空间的偏序规约算法进行深入研究,包括充足集(ample)、持久集(persistent)、条件顽固集(conditional stubborn)。3、基于条件顽固集和持久集的计算算法,通过集合理论证明了在相同条件下,有条件顽固集算法比持久集算法更加有效。4、结合使用顽固集和对称性约简技术,在Petri网的建模工具基础上,分析了读写互斥算法的约简过程,通过工具LoLA进行实验对比验证。5、研究了偏序规约的实验效果评估,并提出了基于Promela语言的领导选举算法的建模方法,同时利用SPIN工具进行偏序规约。
【关键词】：模型检测 偏序规约 顽固集 领导选举
【学位授予单位】：贵州大学
【学位级别】：硕士
【学位授予年份】：2015
【分类号】：TP302.7
【目录】：

• 摘要4-6
• Abstract6-8
• 第1章 绪论8-13
• 1.1 研究背景8-9
• 1.2 研究现状9-10
• 1.3 研究目的及意义10-11
• 1.4 本人工作11
• 1.5 论文结构安排11-13
• 第2章 并发系统的形式化规约及模型检测13-31
• 2.1 软件系统建模13-18
• 2.1.1 并发系统13-14
• 2.1.2 状态和状态空间14-16
• 2.1.3 变迁系统与粒度16-18
• 2.2 形式化分析18-20
• 2.2.1 形式化方法18-19
• 2.2.2 并发系统的形式化描述19-20
• 2.3 模型检测20-24
• 2.3.1 自动机20-22
• 2.3.2 模型检测过程22-23
• 2.3.3 模型检测的优缺点23-24
• 2.4 基于TLA+数学实例的形式化规约24-27
• 2.4.1 TLA和TLA+24-25
• 2.4.2 使用TLA+的数学实例规约25-27
• 2.5 状态爆炸问题27-30
• 2.6 本章小结30-31
• 第3章 利用偏序规约解决状态爆炸问题31-46
• 3.1 偏序规约31-32
• 3.2 独立变迁与迹理论32-34
• 3.3 选择性搜索与并发系统中的独立性34-36
• 3.4 相关偏序算法36-43
• 3.4.1 充足集36-37
• 3.4.2 持久集（算法a）37-39
• 3.4.3 条件顽固集（算法b）39-43
• 3.5 持久集和顽固集的算法比较和证明43-44
• 3.6 本章小结44-46
• 第4章 基于顽固集和对称约简技术的Petri网模型检测方法46-55
• 4.1 Petri网46-47
• 4.2 对称约简技术47-48
• 4.3 结合对称性和顽固集进行状态空间约简48-54
• 4.3.1 工具LoLA简介48-49
• 4.3.2 基于读写互斥算法的检测及结果分析49-54
• 4.4 本章小结54-55
• 第5章 基于偏序规约的SPIN模型检测及应用实例55-63
• 5.1 偏序方法的评估及SPIN的使用55-57
• 5.2 基于领导选举协议的偏序规约57-61
• 5.2.1 领导选举算法介绍57-58
• 5.2.2 对领导选举算法进行建模规约与检测58-61
• 5.3 本章小结61-63
• 第6章 总结与展望63-65
• 6.1 本文工作总结63
• 6.2 展望63-65
• 致谢65-66
• 参考文献66-69
• 附录 A：作者在攻读硕士学位期间的学术论文及参与的科研项目69-70

【参考文献】

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

1 杨琛;房鼎益;陈晓江;;一种有效的分布式构件交互性质验证方法[J];西北大学学报(自然科学版);2007年03期

2 冯登国,范红;安全协议形式化分析理论与方法研究综述[J];中国科学院研究生院学报;2003年04期

，

本文编号：1015994