| 提要 | 第1-7页 |
| 第一章 绪论 | 第7-17页 |
| ·课题背景 | 第7-8页 |
| ·软件验证技术 | 第8-10页 |
| ·软件正确性和可靠性问题 | 第8-9页 |
| ·软件系统的调试、测试和验证 | 第9-10页 |
| ·软件的形式化验证 | 第10页 |
| ·软件模型验证技术 | 第10-12页 |
| ·针对需求分析的软件模型验证 | 第10-11页 |
| ·针对源代码的软件模型验证 | 第11-12页 |
| ·模型检测技术的国内外相关研究 | 第12-15页 |
| ·主要应用于硬件和协议验证的模型检测工具 | 第12-14页 |
| ·最近一段时间国内外关于软件模型验证的研究进展 | 第14-15页 |
| ·本文的研究内容及组织结构 | 第15-17页 |
| 第二章 模型检测技术简介 | 第17-23页 |
| ·模型检测技术的发展 | 第17-18页 |
| ·模型检测基本概念 | 第18-20页 |
| ·模型检测基本思想 | 第18-19页 |
| ·Kripke 模型 | 第19页 |
| ·时态逻辑和其它逻辑 | 第19-20页 |
| ·系统建模和属性建模 | 第20-21页 |
| ·模型检测算法 | 第21-23页 |
| ·LTL 模型检测 | 第21页 |
| ·CTL 模型检测 | 第21-22页 |
| ·OBDD 验证 | 第22-23页 |
| 第三章 协议验证器jlu_PV 及其对软件验证的启发 | 第23-30页 |
| ·jlu_PV 简介 | 第23-24页 |
| ·jlu_PV 的主要思想和采用的主要技术 | 第24-25页 |
| ·主要思想 | 第24页 |
| ·jlu_PV 采用的主要技术 | 第24-25页 |
| ·jlu_PV 的设计与实现 | 第25-27页 |
| ·对软件验证的启发 | 第27-30页 |
| ·协议验证器和软件验证器的共同点和区别 | 第27-28页 |
| ·jlu_PV 对软件验证的借鉴 | 第28-30页 |
| 第四章 软件模型验证技术 | 第30-34页 |
| ·一个软件验证实例 | 第30-31页 |
| ·各种软件验证器的优缺点和借鉴 | 第31-32页 |
| ·程序分析方法的应用 | 第32-34页 |
| ·别名分析 | 第32-33页 |
| ·程序切片 | 第33页 |
| ·信息流分析 | 第33-34页 |
| 第五章 软件验证器jlu_SV 的主要思想和总体框架 | 第34-40页 |
| ·jlu_SV 的主要思想 | 第34-38页 |
| ·CL-Subset 代码转化及其化简 | 第35-36页 |
| ·基于SAT 的软件模型检测方法 | 第36-38页 |
| ·jlu_SV 的框架结构 | 第38-40页 |
| 第六章 jlu_SV 的设计与实现 | 第40-47页 |
| ·CL-Subset 代码转化 | 第40-43页 |
| ·别名分析器 | 第43-44页 |
| ·程序切片 | 第44页 |
| ·构建规划图模块 | 第44-45页 |
| ·命题公式构建 | 第45-47页 |
| 第七章 例子检验、试验结果分析及前景展望 | 第47-50页 |
| ·例子检验 | 第47-49页 |
| ·经验总结及前景展望 | 第49-50页 |
| 第八章 结束语 | 第50-52页 |
| 参考文献 | 第52-57页 |
| 摘要 | 第57-60页 |
| Abstract | 第60-65页 |
| 致谢 | 第65页 |