基于SAT的组合迁移系统模型检测技术研究
| 摘要 | 第1-4页 |
| Abstract | 第4-9页 |
| 主要符号对照表 | 第9-10页 |
| 第1章 绪论 | 第10-23页 |
| ·研究背景 | 第10-14页 |
| ·模型检测 | 第11-13页 |
| ·基于SAT的模型检测 | 第13-14页 |
| ·研究现状 | 第14-19页 |
| ·限界模型检测 | 第15-16页 |
| ·可达集计算 | 第16页 |
| ·时序归纳 | 第16-17页 |
| ·抽象精化 | 第17-19页 |
| ·研究思路 | 第19-20页 |
| ·论文贡献 | 第20-22页 |
| ·论文结构 | 第22-23页 |
| 第2章 基于宏迁移的状态变迁模型 | 第23-44页 |
| ·组合迁移系统 | 第23-26页 |
| ·扩展迁移系统 | 第23-24页 |
| ·组合迁移系统 | 第24-26页 |
| ·宏迁移 | 第26-30页 |
| ·宏迁移的定义 | 第27-29页 |
| ·宏迁移的执行 | 第29-30页 |
| ·基于宏迁移的状态变迁模型 | 第30-35页 |
| ·单模块模型 | 第31-34页 |
| ·多模块组合模型 | 第34-35页 |
| ·正确性证明 | 第35-38页 |
| ·宏迁移执行方式的正确性 | 第36页 |
| ·基于宏迁移的状态变迁模型的正确性 | 第36-38页 |
| ·实验结果 | 第38-41页 |
| ·相关研究工作 | 第41-43页 |
| ·本章小结 | 第43-44页 |
| 第3章 时序归纳算法优化 | 第44-77页 |
| ·基础知识 | 第44-49页 |
| ·SAT求解相关 | 第44-47页 |
| ·时序归纳算法 | 第47-48页 |
| ·增量式时序归纳算法 | 第48-49页 |
| ·子句变换和重用 | 第49-61页 |
| ·表达式变换 | 第50页 |
| ·子句变换和重用机制 | 第50-54页 |
| ·增量式模型检测算法 | 第54-56页 |
| ·实验结果 | 第56-61页 |
| ·搜索树重用 | 第61-71页 |
| ·基于搜索树重用的增量式 SAT 算法 | 第61-63页 |
| ·归纳问题序列的增量式求解 | 第63-68页 |
| ·实验结果 | 第68-71页 |
| ·优化的变量决策 | 第71-76页 |
| ·变量决策策略 | 第72-73页 |
| ·优化的时序归纳算法 | 第73-74页 |
| ·实验结果 | 第74-75页 |
| ·相关工作 | 第75-76页 |
| ·本章小结 | 第76-77页 |
| 第4章 基于极大项覆盖的 SAT 求解 | 第77-92页 |
| ·相关工作 | 第77页 |
| ·算法理论 | 第77-82页 |
| ·优化策略 | 第82-88页 |
| ·实验结果 | 第88-91页 |
| ·本章小结 | 第91-92页 |
| 第5章 工具及其应用 | 第92-103页 |
| ·Tsmart-Beagle简介 | 第92-97页 |
| ·工具概述 | 第92-93页 |
| ·工具设计与实现 | 第93-97页 |
| ·应用案例 | 第97-102页 |
| ·案例1：MTP | 第97-98页 |
| ·案例2：DPU | 第98-99页 |
| ·案例3：GCS | 第99-100页 |
| ·实验结果 | 第100-102页 |
| ·本章小结 | 第102-103页 |
| 第6章 结束语 | 第103-105页 |
| ·工作总结 | 第103-104页 |
| ·研究展望 | 第104-105页 |
| 参考文献 | 第105-110页 |
| 致谢 | 第110-112页 |
| 个人简历、在学期间发表的学术论文与研究成果 | 第112页 |
