基于无穷模型命题投影时序逻辑的模型检查

论文摘要

目前软件工业界面临着产品功能越来越复杂和推出产品周期越来越短的双重压力。软件工程的一个主要目标就是在复杂性增加的情况下仍能构造正确可靠的系统。为了达到上述目标,形式化方法在软件开发中得到了广泛的应用,特别是模型检查技术。本文提出了一种基于命题投影时序逻辑的模型检查方法。在此方法中,系统的性质用命题投影时序逻辑公式来描述,系统模型用Büchi自动机来刻画。通过将描述系统性质的公式转换成Büchi,进而与刻画系统模型的Büchi自动机求积判空来完成模型检查,即检查系统是否满足期望的性质。在基于命题投影时序逻辑公式的模型检查器的设计时,本文将模型检测投影时序逻辑公式与模型检查器SPIN相结合,用PPTL公式来在SPIN中描述系统的性质,这样基于命题投影时序逻辑的模型检查就能在SPIN中完成。

论文目录

• 摘要
• Abstract
• 第一章 绪论
• 1.1 研究背景
• 1.1.1 存在的问题
• 1.1.2 可能的解决方法
• 1.1.3 本文的研究方向
• 1.2 研究现状
• 1.2.1 模型检查技术研究现状
• 1.2.2 时序逻辑研究现状
• 1.3 本文的研究工作和章节安排
• 第二章 模型检查
• 2.1 模型检查原理
• 2.2 模型检查的主要方法
• 2.3 模型检查技术的优点及局限性
• 2.3.1 模型检查技术优点
• 2.3.2 模型检查技术的局限性
• 2.4 缩减状态空间的相关技术
• 2.4.1 状态空间爆炸
• 2.4.2 二叉判定图（BDD）的符号化状态空间表示
• 2.4.3 内存管理策略
• 2.4.4 偏序约简（Partial-order Reduction）
• 2.4.5 等价归约（Reduction through Equivalences）
• 第三章 命题投影时序逻辑
• 3.1 语法
• 3.2 语义
• 3.3 可满足性和有效性
• 3.4 导出公式
• 3.4.1 导出的常用操作符
• 3.4.2 其它导出公式
• 3.5 优先级规则
• 3.6 等价关系
• 3.7 PPTL公式的正则形与可判定性
• 3.7.1 PPTL公式的正则形
• 3.7.2 PPTL公式的可判定性问题
• 第四章 基于无穷模型PPTL公式的模型检查
• 4.1 Büchi 自动机
• 4.2 PPTL公式的正则图
• 4.3 模型检查PPTL公式
• 4.3.1 模型检查PPTL公式总体方案
• 4.3.2 从PPTL公式到Büchi自动机的转化
• 4.3.3 构造积自动机
• 4.3.4 Büchi自动机的判空
• 4.4 本章小结
• 第五章 模型检查器的设计
• 5.1 模型检查PPTL公式与SPIN
• 5.2 模型检查器的设计
• 5.3 实例分析
• 结束语
• 致谢
• 参考文献
• 研究成果