| 摘要 | 第1-4页 |
| ABSTRACT | 第4-9页 |
| 第一章 绪论 | 第9-17页 |
| ·引言 | 第9页 |
| ·课题研究背景 | 第9-15页 |
| ·安全相关软件标准 | 第9-11页 |
| ·软件测试覆盖率 | 第11-13页 |
| ·基于模型的设计方法 | 第13-15页 |
| ·课题开发环境 | 第15页 |
| ·本文研究内容 | 第15-17页 |
| 第二章 软件结构覆盖率分析 | 第17-32页 |
| ·覆盖率分析 | 第18-20页 |
| ·代码结构覆盖率 | 第20-24页 |
| ·语句覆盖 | 第20-22页 |
| ·判定覆盖 | 第22-23页 |
| ·MC/DC 覆盖 | 第23-24页 |
| ·MC/DC 覆盖率分类 | 第24-28页 |
| ·唯一原因法 | 第24-26页 |
| ·屏蔽法 | 第26-27页 |
| ·二者比较 | 第27-28页 |
| ·使用MC/DC 时应注意的问题 | 第28-32页 |
| ·逻辑式中操作符OR 与XOR 的误写 | 第29-30页 |
| ·逻辑式中括号的位置不正确 | 第30页 |
| ·逻辑式中逻辑组元被误写 | 第30-32页 |
| 第三章 基于模型的机车关键软件的设计和验证 | 第32-65页 |
| ·模型覆盖率与代码覆盖率 | 第32-34页 |
| ·代码覆盖率 | 第32页 |
| ·模型覆盖率 | 第32-33页 |
| ·模型覆盖率的作用 | 第33-34页 |
| ·SCADE Suite 简介 | 第34-38页 |
| ·SCADE Suite 的功能模块 | 第35-37页 |
| ·SCADE Suite 与其他工具的桥接 | 第37-38页 |
| ·案例：列车控制系统模式切换功能 | 第38-45页 |
| ·ATP 系统简介 | 第39页 |
| ·ATP 模式切换功能描述 | 第39-44页 |
| ·ATP 模式切换表 | 第44-45页 |
| ·使用SCADE Suite 建立案例功能模型 | 第45-55页 |
| ·类型定义 | 第45-46页 |
| ·常量定义 | 第46-47页 |
| ·主功能模块接口定义 | 第47-52页 |
| ·模块功能实现 | 第52-54页 |
| ·模块框架 | 第54-55页 |
| ·使用SCADE Suite 进行模型验证 | 第55-65页 |
| ·测试环境（SCADE Suite Simulator、MTC） | 第56页 |
| ·测试用例 | 第56-58页 |
| ·覆盖率准则 | 第58-65页 |
| ·默认覆盖率准则 | 第59-61页 |
| ·自定义覆盖率准则 | 第61-65页 |
| 第四章 案例测试结果及相关分析 | 第65-91页 |
| ·项目需求管理 | 第65-68页 |
| ·需求管理工具简介 | 第65-66页 |
| ·概要设计范例 | 第66-67页 |
| ·概要设计范例需求识别 | 第67-68页 |
| ·测试规程&测试用例 | 第68-71页 |
| ·测试规程 | 第68-70页 |
| ·测试用例 | 第70-71页 |
| ·基于需求的覆盖率分析 | 第71-72页 |
| ·软件结构覆盖率分析获取 | 第72-91页 |
| ·模型插装 | 第72页 |
| ·获取模型覆盖率 | 第72-73页 |
| ·模型覆盖率解析 | 第73-85页 |
| ·模型覆盖率报告自动生成 | 第85-91页 |
| 第五章 总结及下一步研究目标 | 第91-95页 |
| ·总结 | 第91-92页 |
| ·下一步研究计划 | 第92-95页 |
| ·源代码追踪 | 第92-93页 |
| ·目标码验证 | 第93-94页 |
| ·研究计划 | 第94-95页 |
| 参考文献 | 第95-99页 |
| 缩略语 | 第99-100页 |
| 致谢 | 第100-101页 |
| 攻读学位期间发表的学术论文目录 | 第101-103页 |