| 致谢 | 第1-6页 |
| 中文摘要 | 第6-8页 |
| ABSTRACT | 第8-15页 |
| 1 引言 | 第15-27页 |
| ·研究背景 | 第15-16页 |
| ·列控系统软件的特点 | 第16-18页 |
| ·列控系统软件测试技术及现状 | 第18-21页 |
| ·列控系统软件安全性测试方法 | 第18-19页 |
| ·列控系统测试用例自动生成方法 | 第19-20页 |
| ·列控系统软件测试遇到的挑战 | 第20-21页 |
| ·安全软件故障相关测试 | 第21-24页 |
| ·安全软件测试方法 | 第21-22页 |
| ·软件故障相关测试序列生成方法 | 第22-24页 |
| ·研究内容和篇章结构 | 第24-27页 |
| 2 相关测试理论与技术 | 第27-37页 |
| ·软件测试用例自动生成方法 | 第27-30页 |
| ·软件测试用例自动生成方法概述 | 第27-29页 |
| ·基于模型的反应式系统测试序列自动生成方法 | 第29-30页 |
| ·一致性测试理论 | 第30-32页 |
| ·模型检验工具选择 | 第32-35页 |
| ·本章小结 | 第35-37页 |
| 3 基于ProcCPN的安全软件异常行为建模方法 | 第37-55页 |
| ·进程模型的描述方法ProcCPN | 第37-45页 |
| ·着色Petri网的相关定义 | 第37-39页 |
| ·进程模型的形式化定义 | 第39-40页 |
| ·进程模型的描述方法ProcCPN | 第40-42页 |
| ·应用ProcCPN方法的实例 | 第42-45页 |
| ·基于ProcCPN的安全软件异常行为分层建模方法 | 第45-49页 |
| ·被测系统SUT模型 | 第46-47页 |
| ·环境模型 | 第47-48页 |
| ·系统模型 | 第48-49页 |
| ·安全软件无死锁和活锁分析 | 第49-52页 |
| ·模型静态死锁避免方法 | 第49-50页 |
| ·基于状态空间的模型无死锁活锁分析 | 第50-52页 |
| ·本章小结 | 第52-55页 |
| 4 故障相关形式化测试序列生成方法 | 第55-85页 |
| ·基本概念定义 | 第55-69页 |
| ·输入输出标号迁移系统IOLTS | 第55-57页 |
| ·被测系统SUT的IOLTS语义 | 第57-60页 |
| ·故障相关测试目的FRTP公式证例路径 | 第60-65页 |
| ·基于ASK-CTL的FRTP | 第65-69页 |
| ·基于FRTP的故障相关形式化测试理论 | 第69-77页 |
| ·形式化-致性测试理论 | 第69-71页 |
| ·基于FROO的一致性测试理论 | 第71-72页 |
| ·故障相关测试序列的形式化定义 | 第72-77页 |
| ·故障相关测试序列FRTS生成方法 | 第77-84页 |
| ·模型正确性检查 | 第77-78页 |
| ·故障相关测试目的公式证例路径生成算法 | 第78-79页 |
| ·故障相关观测目标生成算法 | 第79-80页 |
| ·故障相关测试序列生成算法 | 第80-84页 |
| ·本章小结 | 第84-85页 |
| 5 列控系统车载应用软件测试实例 | 第85-117页 |
| ·列控系统车载应用软件测试方法 | 第85-88页 |
| ·车载应用软件 | 第85-86页 |
| ·车载软件分场景测试方法 | 第86-88页 |
| ·注册与启动场景测试序列生成实例 | 第88-111页 |
| ·注册与启动场景规范 | 第88-90页 |
| ·注册与启动场景形式化模型 | 第90-100页 |
| ·测试序列生成 | 第100-111页 |
| ·测试序列效果分析 | 第111-116页 |
| ·车载设备软件仿真测试平台 | 第111-114页 |
| ·测试执行与结果分析 | 第114-116页 |
| ·本章小结 | 第116-117页 |
| 6 结论 | 第117-119页 |
| ·论文总结 | 第117-118页 |
| ·展望 | 第118-119页 |
| 参考文献 | 第119-131页 |
| 附录A | 第131-135页 |
| 附录B | 第135-141页 |
| 附录C | 第141-143页 |
| 作者简历 | 第143-145页 |
| 攻读博士期间发表论文 | 第145-149页 |
| 学位论文数据集 | 第149页 |