| 致谢 | 第1-6页 |
| 摘要 | 第6-8页 |
| ABSTRACT | 第8-14页 |
| 1 引言 | 第14-24页 |
| ·研究背景 | 第14页 |
| ·典型高速铁路列控系统特性讨论 | 第14-18页 |
| ·典型高速铁路列控系统的共性特征 | 第14-16页 |
| ·高速铁路列控系统相关重要特性 | 第16-17页 |
| ·典型高速铁路列控系统—CTCS-3级列控系统 | 第17-18页 |
| ·高速铁路列控系统的特性验证方法 | 第18-20页 |
| ·选题意义 | 第20页 |
| ·论文结构与写作安排 | 第20-24页 |
| 2 形式化方法在列控系统中的应用 | 第24-34页 |
| ·概述 | 第24-25页 |
| ·基于模型检验的形式化方法 | 第25-27页 |
| ·基于定理证明的形式化方法 | 第27-28页 |
| ·Timed RAISE方法 | 第28-31页 |
| ·RAISE背景和由来 | 第28-29页 |
| ·RAISE描述高速铁路列控系统的优势 | 第29-30页 |
| ·Timed RAISE的引出 | 第30-31页 |
| ·相关形式化方法比较与总结 | 第31-33页 |
| ·小结 | 第33-34页 |
| 3 基于域+Timed RAISE的高速铁路列控系统建模与验证 | 第34-64页 |
| ·复杂系统形式化一般性建模与验证框架 | 第34页 |
| ·基于域+Timed RAISE高速铁路列控系统建模与验证框架 | 第34-36页 |
| ·域以及域组合分解的定义 | 第36-41页 |
| ·域的定义 | 第37-40页 |
| ·域的特性元组分解 | 第40-41页 |
| ·面向高速铁路的CTCS-3级列控系统的域模型 | 第41-49页 |
| ·CTCS-3级列控系统运营场景与域模型间关系讨论 | 第42-44页 |
| ·CTCS-3级列控系统的域模型划分 | 第44-45页 |
| ·CTCS-3级列控系统的域特性分析 | 第45-46页 |
| ·CTCS-3级列控系统域的域特性的组合与分解 | 第46-47页 |
| ·子域的划分 | 第47-49页 |
| ·高速铁路列控系统域特性验证分析 | 第49-53页 |
| ·域模型的Timed RAISE描述分析 | 第53-59页 |
| ·域非特性元组的Timed RAISE描述规则 | 第53-56页 |
| ·域特性元组的Timed RAISE描述规则 | 第56-59页 |
| ·Timed RAISE描述具体验证的流程与规则 | 第59-61页 |
| ·小结 | 第61-64页 |
| 4 基于域的场景交互一致性的验证分析 | 第64-78页 |
| ·RBC切换场景介绍与假设 | 第64-65页 |
| ·RBC切换场景域模型分析 | 第65-67页 |
| ·RBC切换域的验证 | 第67-76页 |
| ·域的相关描述 | 第68-75页 |
| ·域的场景交互一致性分析以及验证 | 第75-76页 |
| ·小结 | 第76-78页 |
| 5 基于域的实时性的验证分析 | 第78-86页 |
| ·等级转换(CTCS-2级至CTCS-3级)基本简介和流程 | 第78-79页 |
| ·等级转换(CTCS-2级至CTCS-3级)域的验证 | 第79-85页 |
| ·域的相关描述 | 第80-84页 |
| ·域的实时性分析以及验证 | 第84-85页 |
| ·小结 | 第85-86页 |
| 6 基于域的安全功能的验证分析 | 第86-111页 |
| ·CTCS-3级列控系统两车追踪控制与系统假设 | 第86-88页 |
| ·CTCS-3级列控系统的两车追踪场景的基本控制过程 | 第86-87页 |
| ·两车追踪场景的基本假设 | 第87-88页 |
| ·追踪场景的安全需求分析 | 第88-93页 |
| ·两车追踪的安全需求 | 第89-90页 |
| ·安全需求基本描述 | 第90-93页 |
| ·安全运行的描述 | 第93页 |
| ·域的描述 | 第93-105页 |
| ·域的输入 | 第94-100页 |
| ·子域的划分 | 第100-105页 |
| ·域的验证 | 第105-109页 |
| ·列车的运行 | 第105-107页 |
| ·两车追踪的初始化 | 第107-109页 |
| ·safe_move的验证 | 第109页 |
| ·小结 | 第109-111页 |
| 7 结论 | 第111-114页 |
| ·论文工作总结 | 第111-112页 |
| ·未来工作展望 | 第112-114页 |
| 参考文献 | 第114-120页 |
| 附录A RBC切换场景验证过程 | 第120-124页 |
| 附录B 等级转换场景验证过程 | 第124-126页 |
| 附录C 两车追踪案例验证过程 | 第126-138页 |
| 作者简历 | 第138-142页 |
| 学位论文数据集 | 第142页 |
