| 摘要 | 第1-6页 |
| Abstract | 第6-12页 |
| 第1章 绪论 | 第12-18页 |
| ·研究背景 | 第12-13页 |
| ·研究意义和目标 | 第13-14页 |
| ·相关研究进展概述 | 第14-15页 |
| ·主要研究内容 | 第15-17页 |
| ·文章导读 | 第17-18页 |
| 第2章 自动生成测试用例方法的研究现状 | 第18-26页 |
| ·特定领域生成测试用例方法现状 | 第18-20页 |
| ·基于有限状态机的测试 | 第18-19页 |
| ·基于标注的转换系统的测试 | 第19页 |
| ·针对面向模型的需求规格说明的测试 | 第19-20页 |
| ·针对面向对象软件的测试 | 第20页 |
| ·运用模型检查生成测试用例方法 | 第20-25页 |
| ·运用模型检查生成测试用例的原理 | 第21-22页 |
| ·主要技术途径 | 第22-23页 |
| ·模型检查方法的优点 | 第23-24页 |
| ·形式化方法目前存在的不足 | 第24-25页 |
| ·本章小结 | 第25-26页 |
| 第3章 基于软件需求建模的测试用例自动生成工具的整体设计框架 | 第26-30页 |
| ·基于软件需求建模的测试用例自动生成工具概貌 | 第26-27页 |
| ·基于软件需求建模的测试用例自动生成工具功能框架设计 | 第27-29页 |
| ·本章小结 | 第29-30页 |
| 第4章 形式化建模功能模块 | 第30-40页 |
| ·形式化建模概述 | 第30-31页 |
| ·需求分析 | 第31-32页 |
| ·形式化模型 | 第32-35页 |
| ·有限状态转换系统 | 第32-34页 |
| ·CTL 时序逻辑 | 第34-35页 |
| ·形式化模型验证 | 第35-36页 |
| ·形式模型的变量标识与跟踪机制研究及工具设计 | 第36-39页 |
| ·本章小结 | 第39-40页 |
| 第5章 时序逻辑CTL 变换功能模块 | 第40-48页 |
| ·测试覆盖准则的意义 | 第40-41页 |
| ·基于模型结构的覆盖准则 | 第41-44页 |
| ·简单转换覆盖 | 第41-42页 |
| ·简单条件覆盖 | 第42页 |
| ·完全条件覆盖 | 第42-43页 |
| ·基于子句的条件覆盖 | 第43-44页 |
| ·时序逻辑变换 | 第44-47页 |
| ·简单转移覆盖的研究及设计实现 | 第44-45页 |
| ·基于MC/DC 覆盖的研究及设计实现 | 第45-47页 |
| ·本章小结 | 第47-48页 |
| 第6章 测试用例自动生成功能模块 | 第48-57页 |
| ·运用模型检查器生成反例 | 第48页 |
| ·形式验证的反例自动提取技术研究及工具设计 | 第48-50页 |
| ·去除冗余反例的算法研究及工具设计 | 第50-53页 |
| ·抽取测试用例 | 第53-56页 |
| ·本章小结 | 第56-57页 |
| 第7章 自动化测试功能模块 | 第57-64页 |
| ·自动化测试的原理 | 第57-60页 |
| ·自动化测试的优点 | 第57-58页 |
| ·测试脚本的种类 | 第58-60页 |
| ·自动化测试的实施 | 第60-63页 |
| ·自动化脚本的设计 | 第60-61页 |
| ·测试驱动文件的设计 | 第61-62页 |
| ·批处理操作及其结果的导出 | 第62-63页 |
| ·本章小结 | 第63-64页 |
| 第8章 实验验证 | 第64-77页 |
| ·净化工作室软件需求简介 | 第64-67页 |
| ·背景知识 | 第64-66页 |
| ·系统运行环境规定 | 第66页 |
| ·系统功能 | 第66-67页 |
| ·针对净化室软件需求的实验验证 | 第67-76页 |
| ·形式化模型导入 | 第68-70页 |
| ·时序逻辑变换 | 第70页 |
| ·模型检查得到反例 | 第70-72页 |
| ·生成测试用例 | 第72-73页 |
| ·自动化测试 | 第73-76页 |
| ·本章小结 | 第76-77页 |
| 结论与展望 | 第77-80页 |
| 参考文献 | 第80-84页 |
| 攻读学位期间发表的学术论文 | 第84-85页 |
| 致谢 | 第85页 |