基于模型检测的UML一致性检验与测试用例生成
| 摘要 | 第1-5页 |
| ABSTRACT | 第5-12页 |
| 第一章 绪论 | 第12-16页 |
| ·研究背景及意义 | 第12-13页 |
| ·国内外研究现状 | 第13-14页 |
| ·论文研究内容 | 第14-15页 |
| ·论文组织结构 | 第15-16页 |
| 第二章 理论背景 | 第16-28页 |
| ·模型检测理论 | 第16-17页 |
| ·模型检测原理 | 第16页 |
| ·模型检测过程 | 第16-17页 |
| ·Kripke 结构 | 第17页 |
| ·时序逻辑 | 第17-19页 |
| ·计算树时序逻辑 CTL* | 第17-18页 |
| ·线性时序逻辑 LTL | 第18页 |
| ·分支时序逻辑 CTL | 第18-19页 |
| ·模型检测工具 NuSMV | 第19-22页 |
| ·NuSMV 的基本结构 | 第19-21页 |
| ·NuSMV 输入语言 SMV | 第21-22页 |
| ·UML 概述 | 第22-24页 |
| ·UML 简介 | 第22页 |
| ·UML 语言体系结构 | 第22-24页 |
| ·UML 模型的一致性 | 第24页 |
| ·软件测试 | 第24-27页 |
| ·软件测试的方法 | 第24-26页 |
| ·测试用例自动生成方法 | 第26-27页 |
| ·本章小结 | 第27-28页 |
| 第三章 UML 顺序图与状态图一致性检验 | 第28-49页 |
| ·UML 与模型检测技术相结合的建模过程 | 第28-29页 |
| ·UML 状态图 | 第29-34页 |
| ·状态图介绍 | 第29-30页 |
| ·状态图语法 | 第30-31页 |
| ·状态图转换 | 第31-34页 |
| ·UML 顺序图 | 第34-37页 |
| ·顺序图介绍 | 第34页 |
| ·顺序图语法 | 第34-35页 |
| ·顺序图转换 | 第35-37页 |
| ·顺序图与状态图的一致性检验 | 第37-38页 |
| ·模型检验工具的实现 | 第38-43页 |
| ·检验工具的设计 | 第38-39页 |
| ·检验工具的实现 | 第39-43页 |
| ·实例应用 | 第43-48页 |
| ·本章小结 | 第48-49页 |
| 第四章 满足 MC/DC 准则的测试用例生成 | 第49-73页 |
| ·运用模型检测生成测试用例的方法 | 第49-51页 |
| ·运用模型检测生成测试用例的原理 | 第49-50页 |
| ·主要技术途径 | 第50-51页 |
| ·基于 MC/DC 准则的时序逻辑构造方法 | 第51-57页 |
| ·MC/DC 准则 | 第51-52页 |
| ·MC/DC 准则的形式化定义 | 第52页 |
| ·MC/DC 准则的算法设计 | 第52-55页 |
| ·算法分析与验证 | 第55-57页 |
| ·运用模型检测生成测试用例的流程 | 第57-64页 |
| ·根据需求规格形式化建模 | 第57-59页 |
| ·根据 MC/DC 准则构造时序逻辑 | 第59-60页 |
| ·运用模型检测工具进行验证 | 第60-62页 |
| ·从反例中提取测试用例 | 第62-64页 |
| ·测试用例自动生成工具的实现与验证 | 第64-72页 |
| ·航空电子系统测试过程 | 第64-65页 |
| ·测试用例生成工具的设计 | 第65-66页 |
| ·测试用例生成工具的实现与验证 | 第66-70页 |
| ·在 TestBed 中执行测试用例 | 第70-72页 |
| ·本章小结 | 第72-73页 |
| 第五章 总结与展望 | 第73-75页 |
| ·全文总结 | 第73页 |
| ·未来展望 | 第73-75页 |
| 参考文献 | 第75-79页 |
| 致谢 | 第79-80页 |
| 在学期间的研究成果及发表的学术论文 | 第80页 |
