基于GSTE理论的抽象与细化问题的研究
| 摘要 | 第1-5页 |
| ABSTRACT | 第5-10页 |
| 第一章 绪论 | 第10-22页 |
| ·课题背景 | 第10-11页 |
| ·形式化验证 | 第11-16页 |
| ·形式化验证的基本概念和原理 | 第11-15页 |
| ·形式化验证方法的意义以及不足 | 第15-16页 |
| ·形式化验证方法的发展 | 第16-19页 |
| ·抽象方法的提出以及意义 | 第16-17页 |
| ·模型验证方法 | 第17-18页 |
| ·有界模型验证 | 第18-19页 |
| ·无界模型检验 | 第19页 |
| ·研究意义 | 第19-20页 |
| ·主要研究内容和章节安排 | 第20-22页 |
| ·主要研究内容 | 第20页 |
| ·章节安排 | 第20-22页 |
| 第二章 符号轨迹赋值和推广化轨迹赋值简介 | 第22-40页 |
| ·电路模型 | 第22-24页 |
| ·硬件电路的功能模型 | 第22-23页 |
| ·硬件电路的结构模型 | 第23-24页 |
| ·符号轨迹赋值(STE)介绍 | 第24-31页 |
| ·STE 电路模型的定义 | 第25-26页 |
| ·STE 验证规范的相关概念 | 第26-28页 |
| ·STE 验证算法过程 | 第28-30页 |
| ·STE 的优点与不足 | 第30-31页 |
| ·推广化符号轨迹赋值(GSTE)介绍 | 第31-38页 |
| ·GSTE 电路模型以及性质描述 | 第31-34页 |
| ·GSTE 验证算法 | 第34-38页 |
| ·GSTE 和STE 检验方法的比较 | 第38-39页 |
| ·本章小结 | 第39-40页 |
| 第三章 抽象与细化方法的研究 | 第40-62页 |
| ·符号处理技术 | 第40-45页 |
| ·二叉判定图 | 第40-44页 |
| ·四值逻辑编码 | 第44-45页 |
| ·抽象的相关概念以及原理 | 第45-54页 |
| ·抽象的相关定义以及分类 | 第46-48页 |
| ·抽象方法 | 第48-54页 |
| ·细化处理 | 第54-57页 |
| ·符号常量 | 第55-56页 |
| ·符号变量 | 第56-57页 |
| ·抽象及细化方法在GSTE 中的应用 | 第57-61页 |
| ·本章小结 | 第61-62页 |
| 第四章 GSTE 抽象与细化方法的改进 | 第62-82页 |
| ·问题来源 | 第62页 |
| ·抽象与细化问题分析 | 第62-66页 |
| ·四值模型抽象的问题分析 | 第62-64页 |
| ·GSTE 抽象细化的问题分析 | 第64-66页 |
| ·GSTE 算法改进 | 第66-72页 |
| ·变量划分算法 | 第66-69页 |
| ·参数化表示和提取算法 | 第69-72页 |
| ·GSTE 抽象细化处理算法改进 | 第72-77页 |
| ·改进GSTE 的软件框架 | 第72-74页 |
| ·改进的GSTE 关键代码 | 第74-77页 |
| ·算法分析及验证 | 第77-81页 |
| ·对变量划分的算法的分析 | 第77页 |
| ·对参数化表示算法的分析 | 第77-79页 |
| ·算法验证 | 第79-81页 |
| ·本章小结 | 第81-82页 |
| 第五章 结论与展望 | 第82-84页 |
| ·本文总结 | 第82-83页 |
| ·主要研究成果和创新点 | 第82-83页 |
| ·存在的不足 | 第83页 |
| ·工作的展望 | 第83-84页 |
| 致谢 | 第84-85页 |
| 参考文献 | 第85-89页 |
| 个人简历及硕士期间取得的学术成果 | 第89-90页 |