列控系统临时限速的形式化分析与异常诊断方法研究
| 摘要 | 第5-6页 |
| abstract | 第6-7页 |
| 第1章 绪论 | 第10-15页 |
| 1.1 背景及研究意义 | 第10-11页 |
| 1.1.1 论文背景 | 第10页 |
| 1.1.2 研究意义 | 第10-11页 |
| 1.2 研究现状 | 第11-14页 |
| 1.2.1 形式化方法研究现状 | 第11-12页 |
| 1.2.2 故障诊断技术研究现状 | 第12-13页 |
| 1.2.3 临时限速故障诊断研究现状 | 第13-14页 |
| 1.3 论文内容及章节安排 | 第14-15页 |
| 第2章 临时限速系统概述 | 第15-22页 |
| 2.1 临时限速系统构成及特点 | 第15页 |
| 2.2 临时限速命令传输流程 | 第15-17页 |
| 2.3 临时限速系统信息交互 | 第17-18页 |
| 2.4 临时限速命令操作流程 | 第18-21页 |
| 2.4.1 临时限速命令的拟定 | 第19页 |
| 2.4.2 临时限速命令的设置 | 第19-20页 |
| 2.4.3 临时限速命令的取消 | 第20-21页 |
| 2.5 本章小节 | 第21-22页 |
| 第3章 临时限速的形式化建模与验证 | 第22-38页 |
| 3.1 时间自动机基础理论 | 第22-23页 |
| 3.2 临时限速系统时间自动机网络 | 第23-30页 |
| 3.2.1 成员自动机模型架构 | 第24-27页 |
| 3.2.2 成员自动机模型建立 | 第27-30页 |
| 3.3 临时限速工作流程模型时序仿真 | 第30-33页 |
| 3.3.1 命令拟定时序仿真 | 第30-31页 |
| 3.3.2 命令设置时序仿真 | 第31-32页 |
| 3.3.3 命令取消时序仿真 | 第32-33页 |
| 3.4 临时限速工作流程模型验证 | 第33-37页 |
| 3.4.1 UPPAAL验证器 | 第33-34页 |
| 3.4.2 形式化验证 | 第34-37页 |
| 3.5 本章小结 | 第37-38页 |
| 第4章 基于图论的临时限速异常的分析与诊断 | 第38-52页 |
| 4.1 基于图论的临时限速系统建模 | 第38-44页 |
| 4.1.1 提取系统节点 | 第39-40页 |
| 4.1.2 节点测试机制 | 第40-41页 |
| 4.1.3 建立测试模型 | 第41-44页 |
| 4.1.4 诊断可行性分析 | 第44页 |
| 4.2 PMC模型诊断方法设计 | 第44-48页 |
| 4.2.1 测试无效模型 | 第44-45页 |
| 4.2.2 诊断规则 | 第45-46页 |
| 4.2.3 诊断流程 | 第46-48页 |
| 4.3 诊断方法验证 | 第48-50页 |
| 4.4 诊断方法性能及特点 | 第50-51页 |
| 4.4.1 诊断方法性能 | 第50-51页 |
| 4.4.2 诊断方法特点 | 第51页 |
| 4.5 本章小结 | 第51-52页 |
| 第5章 基于贝叶斯网络的临时限速异常的分析与推理 | 第52-69页 |
| 5.1 基于贝叶斯网络的临时限速系统建模 | 第52-59页 |
| 5.1.1 故障树模型建立 | 第53-55页 |
| 5.1.2 故障树分析 | 第55-58页 |
| 5.1.3 故障树模型转换 | 第58-59页 |
| 5.2 贝叶斯网络推理 | 第59-64页 |
| 5.2.1 BN条件概率分布 | 第59-60页 |
| 5.2.2 联结树精确推理过程 | 第60-63页 |
| 5.2.3 联结树精确推理结果 | 第63-64页 |
| 5.3 推理方法验证 | 第64-67页 |
| 5.4 推理方法性能及特点 | 第67-68页 |
| 5.4.1 推理方法性能 | 第67-68页 |
| 5.4.2 推理方法特点 | 第68页 |
| 5.5 本章小结 | 第68-69页 |
| 结论 | 第69-71页 |
| 致谢 | 第71-72页 |
| 参考文献 | 第72-76页 |
| 攻读硕士学位期间发表的论文 | 第76页 |
