| 插图索引 | 第1-9页 |
| 表格索引 | 第9-10页 |
| 摘要 | 第10-12页 |
| ABSTRACT | 第12-15页 |
| 第一章 绪论 | 第15-29页 |
| ·研究背景 | 第15页 |
| ·模型检验方法概述 | 第15-22页 |
| ·系统描述 | 第16-17页 |
| ·断言描述 | 第17页 |
| ·模型检验算法 | 第17-20页 |
| ·成功后处理 | 第20-22页 |
| ·问题的提出和相关研究 | 第22-25页 |
| ·反例压缩 | 第22-23页 |
| ·错误定位方法 | 第23-24页 |
| ·为反例标注证明步骤 | 第24页 |
| ·其他方法 | 第24-25页 |
| ·本文的主要工作和创新 | 第25-27页 |
| ·论文结构 | 第27-29页 |
| 第二章 基于迭代式证例搜索的错误定位方法 | 第29-40页 |
| ·引言 | 第29-30页 |
| ·背景知识 | 第30-31页 |
| ·反事实、距离度量与原因 | 第30-31页 |
| ·伪布尔SAT | 第31页 |
| ·模型检验与限界模型检验 | 第31页 |
| ·并列最近证例对定位精度的影响以及解决方法 | 第31-32页 |
| ·错误定位算法 | 第32-37页 |
| ·算法整体流程 | 第32-33页 |
| ·谓词提取 | 第33页 |
| ·证例搜索 | 第33-35页 |
| ·谓词过滤 | 第35-36页 |
| ·证例屏蔽 | 第36-37页 |
| ·实验结果及分析 | 第37-39页 |
| ·精确性度量 | 第37页 |
| ·实验对象简介 | 第37-38页 |
| ·实验结果 | 第38页 |
| ·结果分析 | 第38-39页 |
| ·结论 | 第39-40页 |
| 第三章 基于悖论分析和增量式求解的快速反例压缩算法 | 第40-51页 |
| ·引言 | 第40-41页 |
| ·背景知识 | 第41-43页 |
| ·限界模型检验 | 第41-42页 |
| ·SAT求解器中的冲突学习机制 | 第42页 |
| ·BFL反例压缩算法及其问题 | 第42-43页 |
| ·基于悖论分析的反例压缩算法 | 第43-46页 |
| ·算法概述 | 第43-44页 |
| ·悖论分析 | 第44-45页 |
| ·正确性证明 | 第45-46页 |
| ·复杂性分析 | 第46页 |
| ·增量式SAT求解方法 | 第46-47页 |
| ·实验结果及分析 | 第47-49页 |
| ·试验对象 | 第47页 |
| ·试验方法 | 第47-48页 |
| ·试验结果 | 第48-49页 |
| ·结果分析 | 第49页 |
| ·结论 | 第49-51页 |
| 第四章 低存储开销的反例压缩算法 | 第51-59页 |
| ·引言 | 第51-52页 |
| ·背景知识 | 第52-53页 |
| ·SAT求解器 | 第52页 |
| ·模型检验及反例 | 第52-53页 |
| ·BFL反例压缩算法 | 第53页 |
| ·步进的BFL | 第53-56页 |
| ·问题分解 | 第53-54页 |
| ·子问题求解 | 第54-55页 |
| ·复杂度分析 | 第55-56页 |
| ·步进的单位核提取 | 第56-57页 |
| ·实验结果及讨论 | 第57-58页 |
| ·结论 | 第58-59页 |
| 第五章 非确定系统中不变断言的反例压缩 | 第59-71页 |
| ·引言 | 第59-60页 |
| ·背景知识 | 第60-63页 |
| ·SAT求解器 | 第60页 |
| ·模型检验 | 第60-61页 |
| ·状态集合的立方表示 | 第61-62页 |
| ·基于SAT的前置映象运算 | 第62-63页 |
| ·确定系统的反例压缩 | 第63页 |
| ·非确定系统的反例压缩原理 | 第63-65页 |
| ·压缩反例的标准 | 第63-64页 |
| ·确定与非确定系统的区别 | 第64页 |
| ·压缩反例的定义 | 第64-65页 |
| ·算法的实现、证明与复杂性分析 | 第65-69页 |
| ·算法描述 | 第65-67页 |
| ·正确性证明 | 第67-68页 |
| ·算法复杂度 | 第68-69页 |
| ·实验结果及分析 | 第69-70页 |
| ·结论 | 第70-71页 |
| 第六章 完备的ACTL反例压缩算法 | 第71-81页 |
| ·引言 | 第71-72页 |
| ·背景知识 | 第72-76页 |
| ·二叉决策图(Binary Decision Diagrams) | 第72页 |
| ·CTL时态逻辑 | 第72-73页 |
| ·模型检验 | 第73-74页 |
| ·公平约束 | 第74-75页 |
| ·反例产生 | 第75-76页 |
| ·状态集合的立方表示 | 第76页 |
| ·路径证例压缩算法 | 第76-77页 |
| ·EX证例压缩 | 第76-77页 |
| ·EU证例压缩 | 第77页 |
| ·EG环形证例压缩 | 第77-79页 |
| ·Loop压缩 | 第77-79页 |
| ·Stem压缩 | 第79页 |
| ·实验结果 | 第79-80页 |
| ·结论 | 第80-81页 |
| 第七章 错误定位与反例压缩原型系统的实现 | 第81-93页 |
| ·NuSMV模型检验器 | 第81-83页 |
| ·Zchaff求解器 | 第83-85页 |
| ·基本数据结构和操作 | 第83-84页 |
| ·增量式求解机制 | 第84-85页 |
| ·PBS伪布尔求解器 | 第85-86页 |
| ·非完备错误定位原型系统 | 第86-90页 |
| ·谓词提取 | 第87-88页 |
| ·生成断言和反断言的CNF文件 | 第88页 |
| ·提取信号映射关系、提取反例谓词赋值 | 第88-89页 |
| ·生成证例约束 | 第89页 |
| ·PBS最近证例搜索 | 第89页 |
| ·谓词差异提取 | 第89-90页 |
| ·广度优先代码搜索 | 第90页 |
| ·完备的反例压缩原型系统 | 第90-93页 |
| ·生成断言的CNF文件 | 第90-91页 |
| ·提取信号映射关系 | 第91页 |
| ·目标取反 | 第91页 |
| ·添加完全约束 | 第91页 |
| ·选择尚未被剔除的变量v，并删除v的赋值短句 | 第91页 |
| ·添加v的赋值短句 | 第91页 |
| ·剔除悖论分析结果 | 第91-93页 |
| 第八章 结语 | 第93-97页 |
| ·本文主要贡献 | 第93-94页 |
| ·对今后研究工作的展望 | 第94-97页 |
| ·在非完备的反例解释方面： | 第95页 |
| ·在完备性反例压缩方面 | 第95-96页 |
| ·在错误改正方面 | 第96-97页 |
| 攻读博士期间已发表录用和撰写的论文 | 第97-99页 |
| 攻读博士期间参与的主要科研项目 | 第99-100页 |
| 致谢 | 第100-102页 |
| 参考文献 | 第102-112页 |