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

摘要

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

目录

封面

声明

目录

中文摘要

英文摘要

第1章 绪论

1.1 研究背景

1.2 研究现状

1.3 研究目的及意义

1.4 本人工作

1.5 论文结构安排

第2章 并发系统的形式化规约及模型检测

2.1 软件系统建模

2.2 形式化分析

2.3 模型检测

2.4 基于TLA+数学实例的形式化规约

2.5 状态爆炸问题

2.6 本章小结

第3章 利用偏序规约解决状态爆炸问题

3.1 偏序规约

3.2 独立变迁与迹理论

3.3 选择性搜索与并发系统中的独立性

3.4 相关偏序算法

3.5持久集和顽固集的算法比较和证明

3.6 本章小结

第4章 基于顽固集和对称约简技术的Petri网模型检测方法

4.1 Petri网

4.2 对称约简技术

4.3 结合对称性和顽固集进行状态空间约简

4.4 本章小结

第5章 基于偏序规约的SPIN模型检测及应用实例

5.1 偏序方法的评估及SPIN的使用

5.2 基于领导选举协议的偏序规约

5.3 本章小结

第6章 总结与展望

6.1 本文工作总结

6.2 展望

致谢

参考文献

附录A：作者在攻读硕士学位期间的学术论文及参与的科研项目