基于模型的城际铁路列控系统运营场景仿真与验证

摘要

随着列车运行控制相关技术的发展，列控系统不断融合先进的计算机技术、网络技术以及通信技术，系统的自动化程度不断提高、软硬件规模不断扩大，呈现出复杂的系统特性。作为复杂的安全苛求系统，如何确保列控系统的正确性是重要的研究课题。一方面，Simulink/Stateflow支持图形化建模与仿真，可在系统的前期设计开发中排除部分安全隐患。另一方面，基于严格数学定义的形式化方法能精确，清晰地描述系统的结构和属性，已成为保障列控系统安全的重要手段。因此仿真模型辅以形式化技术为列控系统的建模和验证提供了一种新的思路。
　　本文从城际铁路列控系统的混成属性入手，研究列控系统运营场景的建模与验证，提出了一个集建模、仿真与验证为一体的保障列控系统安全的方法。主要开展了以下相关工作:
　　(1)针对城际铁路列控系统的混成属性，研究了基于Simulink/Stateflow的列控系统运营场景的建模与仿真。建立了城际铁路列控系统的分层模型;引入场景分析方法描述列控系统中各设备对象的典型功能活动以及信息交互，并给出了列控系统运营场景的建模与仿真流程。
　　(2)基于混成自动机理论，研究了对仿真模型辅以形式化验证以保障城际铁路列控系统正确性的方法。方法中对Simulink/Stateflow模型和混成自动机模型的形式化语义进行分析，制定了二者间的模型转换规则，以保证模型转换过程中模型的一致性，并给出了基于SpaceEx验证平台的场景模型的验证流程。
　　(3)在MATLAB环境中构建了列车自动运行场景的仿真平台。仿真平台以真实线路作为底层数据驱动，对模型产生的紧急制动距离与试验中的真实数据进行对比分析;对不同参数组合情况下的列车行为进行仿真分析，并复现了在实际测试现场发现的安全隐患。
　　(4)以城际铁路列控系统典型的列车自动运行场景为案例进行分析，运用提出的模型转换规则将所建立的列车自动运行场景仿真模型转换为混成自动机模型;在SpaceEx混成系统验证工具中建立混成自动机模型，并对系统验证属性进行验证分析，证明了论文提出的建模和验证方法的有效性。

目录

声明

致谢

摘要

1．1 研究背景及意义

1．2 城际铁路CTCS2+ATO列控系统概述

1．2．1 C2+ATO列控系统简介

1．2．2 C2+ATO列控系统与其他信号系统的比较

1．3 列控系统建模仿真与验证方法国内外研究现状

1．3．1 国内外列控系统建模仿真方法研究现状

1．3．2 国内外列控系统形式化验证的研究现状

1．3．3 论文研究内容

1．3．4 论文结构

2 城际铁路列控系统运营场景的建模仿真与验证方法分析

2．1 城际铁路列控系统的运营场景概述

2．1．1 场景概念与描述

2．1．2 C2+ATO列控系统运营场景

2．2 城际铁路列控系统运营场景的建模及仿真方法

2．2．1 混成系统简介

2．2．2 Simulink和Stateflow简介

2．2．3 基于Simulink／Stateflow的列控系统运营场景建模方法

2．3 针对仿真模型辅以形式化验证方法

2．3．1 混成自动机理论简介

2．3．2 SLSF模型与HA模型的转换规则

2．3．3 混成属性的验证

2．4 本章小结

3 列车自动运行场景的建模与仿真

3．1 列车自动运行场景概述

3．2 列车自动运行场景的SLSF模型

3．2．1 列车模型

3．2．2 车载控制子系统模型

3．2．3 TCC子系统模型

3．2．4 CTC子系统模型

3．3 列车自动运行场景仿真及分析

3．3．1 模型参数和仿真参数设置

3．3．2 紧急制动距离验证与分析

3．3．3 不同组合参数下场景的仿真与分析

3．4 本章小结

4 列车自动运行场景模型的验证与分析

4．1 模型假设

4．2 场景模型转换

4．2．1 ATP超速防护功能模型转换

4．2．2 ATO自动驾驶功能模型转换

4．2．3 TCC功能模型转换

4．3 场景功能模型验证及站内不停车案例验证

4．3．1 混成系统验证工具SpaceEX

4．3．2 基于SpaceEX的列车自动运行场景建模

4．3．3 场景功能模型验证及结果分析

4．3．4 站内不停车实例验证与结果分析

4．4 本章小结

5．1 全文工作总结

5．2 研究工作展望

参考文献

表索引

图索引

作者简历及攻读硕士学位期间取得的研究成果

学位论文数据集