文摘
英文文摘
声明
第一章绪论
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二叉判定图(BBD)的符号化状态空间表示
2.4.3内存管理策略
2.4.4偏序约简(Partial-order Reduction)
2.4.5等价归约(Reductionthrough 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实例分析
结束语
致谢
参考文献
研究成果