列车运行控制系统(简称列控系统)是保证铁路运输安全、提高运输效率的核心技术装备，是铁路运输的“大脑和神经中枢”。随着计算机和电子设备在列控系统中的应用，越来越多的安全功能由软件来承载，使得列控系统呈现出与传统铁路信号设备不同的特征。系统复杂度越来越高，子系统间通信交互越来越频繁，系统运行从封闭的静态环境延伸到开放、动态的分布式环境，环境中存在大量不确定性因素等导致实现对列车运行精确安全的控制变得非常困难。随着通信技术及计算机智能技术的进一步发展，未来列控系统将呈现一体化、智能化、自动化等特点，系统功能紧耦合，行车指挥实时动态调整，列车全自动运行等场景的出现更进一步增加了列控系统实现安全控制的难度。面对新形势下列控系统，如何对其典型特征进行分析及建模，针对复杂大规模列控系统模型行为进行高效验证成为保证列车安全运行亟需解决的问题。
　　本文以现阶段高铁列控系统及其未来发展趋势为背景，针对列控系统安全性保障问题，主要研究从列控系统自身行为特征出发的建模及验证方法。面向列控系统的特征，建立一套适用于列控系统的形式规约，以列控系统特点为基础进行建模，使系统模型最大限度贴近实际物理对象及其行为，并根据系统模型提出高效的验证方法。具体来说，本文取得了如下创新：
　　(1)针对列控系统数据安全问题，建立了基于图论的列控数据模型，提出了一种列控进路数据正确性的验证方法。从列控系统数据与控制逻辑相分离的设计理念出发，研究了列控拓扑元素及其关联关系，给出了列控静态数据的形式化规约。基于列控拓扑元素的逻辑关联关系，建立了基于图论的列控数据统一模型。在该模型的基础上，提出了数据安全性验证的若干定理，并进行了理论证明。从理论上为列控逻辑数据提供了一种形式化的精确刻画手段，可有效支撑列控数据自动化验证。
　　(2)针对列控安全逻辑形式规约问题，提出了一种基于拓扑流形理论的列车安全控制逻辑形式规约方法。对列车实时动态运行行为曲线及列车运行限制曲线进行形式化描述，给出了基于拓扑流形的安全线路条件约束，建立了列车动态间隔运行控制移动授权逻辑模型，并证明了控制逻辑模型的安全性。利用拓扑流形理论解决了考虑列车动态运行行为的控制逻辑形式规约问题。
　　(3)针对传统方法无法处理大规模系统验证的问题，基于拓扑流形理论，提出了一种适用于列控系统安全控制逻辑的运行时验证方法。在安全逻辑形式规约的基础上，以动态间隔运行控制方式列控系统为对象，提出了列控实时数据正确性、控制逻辑安全性、以及列车在控制指令安全性定理，并给出了理论证明和监控算法。为列车动态间隔控制逻辑的安全保障提供了一套新的方法。
　　(4)针对列控系统混成特征难于验证的问题，综合考虑列车运行的连续行为与离散状态，提出了一种基于可达集分析的列车超速防护混成监控方法。以CTCS-3列控系统超速防护逻辑为对象，建立了系统的动态参数模型。根据列车运行信息实时更新模型的对应参数，通过计算列车运行行为可达集实现对列车的动态连续监控，提高了监控的精确性，为列控系统混成验证提供了一种有效手段。
　　本文立足于列控系统的特征，提出了一套列控数据及安全控制逻辑的建模与验证方法，并结合实际线路数据进行了实例分析及仿真验证，实验结果表明所提方法有效的解决了列控系统数据及控制逻辑的模型构建及安全性验证问题。本文工作为未来列控系统的高效开发与系统安全保障提供理论方法支撑。