| 摘要 | 第1-6页 |
| ABSTRACT | 第6-11页 |
| 第1章 绪论 | 第11-16页 |
| ·研究背景 | 第11页 |
| ·研究意义和目标 | 第11-13页 |
| ·相关研究进展概述 | 第13-14页 |
| ·主要研究内容 | 第14-16页 |
| 第2章 测试用例自动生成方法的研究现状 | 第16-24页 |
| ·基于有限状态机的测试 | 第16页 |
| ·基于标注的转换系统的测试 | 第16-17页 |
| ·针对面向模型的需求规格说明的测试 | 第17页 |
| ·针对面向对象软件的测试 | 第17-18页 |
| ·运用模型检查生成测试用例方法 | 第18-22页 |
| ·运用模型检查生成测试用例的原理 | 第18-20页 |
| ·主要技术途径 | 第20-21页 |
| ·采用模型检查方法的优点 | 第21页 |
| ·形式化方法目前存在的不足 | 第21-22页 |
| ·国内相关研究现状 | 第22-23页 |
| ·本章小结 | 第23-24页 |
| 第3章 针对模型检查技术的改进措施 | 第24-26页 |
| ·模型检查与基于路径的测试方法的结合 | 第24页 |
| ·运用有界整型数据模拟浮点型数据 | 第24-25页 |
| ·本章小结 | 第25-26页 |
| 第4章 测试覆盖准则的制定 | 第26-33页 |
| ·模型元素的形式化定义 | 第26-28页 |
| ·状态空间 | 第26页 |
| ·转换 | 第26-28页 |
| ·转换集合 | 第28页 |
| ·基本的转换系统 | 第28页 |
| ·基于模型结构的覆盖准则 | 第28-31页 |
| ·简单转换覆盖 | 第29页 |
| ·简单条件覆盖 | 第29-30页 |
| ·完全条件覆盖 | 第30页 |
| ·基于子句的条件覆盖 | 第30-31页 |
| ·本章小结 | 第31-33页 |
| 第5章 基于MC/DC 准则的时序逻辑构造方法的实现 | 第33-44页 |
| ·时序逻辑语法 | 第34-35页 |
| ·表达式分析树方法的应用 | 第35-36页 |
| ·构造满足MC/DC 准则的时序逻辑的算法 | 第36-38页 |
| ·程序实现 | 第38-42页 |
| ·本章小结 | 第42-44页 |
| 第6章 测试用例自动生成的运行流程 | 第44-52页 |
| ·形式化建模 | 第44-48页 |
| ·需求分析 | 第45-46页 |
| ·形式化模型的SMV 描述 | 第46-47页 |
| ·模型验证 | 第47-48页 |
| ·模型中状态迁移的描述 | 第48-49页 |
| ·时序逻辑变换 | 第49-50页 |
| ·用例的自动生成 | 第50-51页 |
| ·运用模型检查器生成反例 | 第51页 |
| ·从反例中提取用例 | 第51页 |
| ·本章小结 | 第51-52页 |
| 第7章 自动生成方法的实验验证 | 第52-75页 |
| ·智能电源控制器软件需求简介 | 第52-53页 |
| ·针对智能电源控制器需求的形式化建模 | 第53-62页 |
| ·建模对象的选取 | 第53-54页 |
| ·针对需求输入数据的简化与抽象 | 第54-55页 |
| ·针对需求中浮点型输入数据的建模 | 第55-62页 |
| ·用例生成 | 第62-73页 |
| ·运用时序逻辑描述模型中的状态迁移 | 第62页 |
| ·依据简单转换覆盖准则指导测试用例的生成 | 第62-65页 |
| ·依据基于子句的条件覆盖准则指导测试用例的生成 | 第65-73页 |
| ·实验结论分析 | 第73-74页 |
| ·本章小结 | 第74-75页 |
| 结论与展望 | 第75-77页 |
| 参考文献 | 第77-83页 |
| 攻读学位期间发表的学术论文 | 第83-84页 |
| 致谢 | 第84页 |