| 摘要 | 第1-6页 |
| Abstract | 第6-15页 |
| 第一章 绪论 | 第15-24页 |
| ·研究背景 | 第15-20页 |
| ·混成系统 | 第15-16页 |
| ·可靠性保障 | 第16-17页 |
| ·模型检验 | 第17-20页 |
| ·研究问题 | 第20-21页 |
| ·主要工作 | 第21-22页 |
| ·论文组织结构 | 第22-24页 |
| 第二章 线性混成自动机面向路径有界可达性检验 | 第24-34页 |
| ·线性混成自动机定义 | 第24-25页 |
| ·路径、行为及可达性 | 第25-27页 |
| ·可达性检验 | 第27页 |
| ·有界可达性检验 | 第27-29页 |
| ·组合自动机的可达性检验 | 第29-31页 |
| ·组合自动机的有界可达性检验 | 第31-33页 |
| ·本章小结 | 第33-34页 |
| 第三章 SAT-ⅡS-LP联合反馈制导的状态空间约减 | 第34-55页 |
| ·SAT-ⅡS-LP联合反馈制导的有界可达性检验 | 第34-37页 |
| ·有界图结构的SAT编码 | 第37-39页 |
| ·SAT-LP联合的有界可达性检验 | 第39页 |
| ·基于ⅡS技术的路径枚举加速 | 第39-44页 |
| ·实例研究 | 第44-51页 |
| ·相关工作 | 第51-54页 |
| ·本章小结 | 第54-55页 |
| 第四章 基于组合ⅡS路径抽取的遍历优化 | 第55-72页 |
| ·组合ⅡS路径定位 | 第55-58页 |
| ·基于SMT编码的有界图结构遍历 | 第58-61页 |
| ·多重ⅡS路径定位技术 | 第61-63页 |
| ·实验配置与性能评估 | 第63-70页 |
| ·相关工作 | 第70-71页 |
| ·本章小结 | 第71-72页 |
| 第五章 基于有界可达性检验的全局性质推导 | 第72-90页 |
| ·基于线性时序逻辑的有界可达性检验全局性质推导 | 第72-82页 |
| ·延时证明 | 第75-77页 |
| ·立时证明 | 第77-82页 |
| ·实验评估 | 第82-88页 |
| ·与同类工具的比较 | 第83-85页 |
| ·基于立时证明的优化 | 第85-88页 |
| ·相关工作 | 第88-89页 |
| ·本章小结 | 第89-90页 |
| 第六章 非线性混成自动机有界可达性检验 | 第90-99页 |
| ·非线性混成自动机定义 | 第90-91页 |
| ·路径、行为及面向路径可达性定义 | 第91-93页 |
| ·面向路径可达性检验方法 | 第93-94页 |
| ·不可行子路径片段抽取 | 第94-97页 |
| ·面向路径有界可达性检验优化 | 第97页 |
| ·本章小结 | 第97-99页 |
| 第七章 全文总结 | 第99-102页 |
| ·论文的主要工作 | 第99-100页 |
| ·进一步的工作 | 第100-102页 |
| 参考文献 | 第102-112页 |
| 简历与科研成果 | 第112-114页 |
| 致谢 | 第114-116页 |