近年来,我国高速铁路快速发展,列控系统不断融合先进的计算机技术、网络技术以及通信技术,使得系统的自动化程度不断提高、软硬件规模不断扩大,呈现出复杂的系统特性。作为复杂的安全苛求系统,如何确保列控系统的正确性是重要的研究课题。自主化CTCS-3级列控系统相比于过去的国产化CTCS-3级列控系统,硬件、软件完全自主研发,拥有自主产权,同时在功能需求上也提出了新要求,这就需要依据新的规范对自主化CTCS-3级列控系统进行新的场景分析。为了确保证系统的安全性和CTCS-3列控系统的跨线运营能力,本文从列控系统的实时性入手,研究列控系统场景的建模与验证,主要开展了以下相关工作:(1)通过比较多种验证系统实时性的形式化方法,选择时间自动机理论来验证系统的实时性,并介绍了时间自动机理论及其模型检验工具UPPAAL的使用方法。(2)以码序校验场景和复杂场景为例,分析各场景下系统设备的工作流程,根据研究对象的特点,在合理的抽象和假设之后,利用时间自动机理论分别建立了码序校验场景工作流程、复杂场景工作流程的时间自动机模型。(3)应用UPPAAL验证工具对码序校验场景、复杂场景下系统进行分析验证:通过设置通道和全局变量,构造了时间自动机的积;使用模拟器,对个场景下设备的交互情况进行仿真,分析列车运行过程中的状态变化;使用验证器,验证了系统的安全性、实时性和功能性,证明了该建模验证方法的有效性。(4)结合大西高铁综合试验数据,分析、提取各个厂家自主化CTCS-3级列控系统设备在运营场景中信息交互的流程,采用实际的线路数据编写测试序列;同时,在实验室既有CTCS-3级列控系统互联互通测试平台的基础上,通过对平台软件的修改使之适用于自主化CTCS-3级列控系统,并开展仿真测试验证。