自主化CTCS-3级列控系统在确保高铁列车的安全运行方面起着至关重要的作用,有完全的自主产权,在软硬件设计以及功能需求上都新增了许多内容。因此,如何确保列控系统在新增规范要求下的安全性和可靠性就成为了重要的研究课题。同时对采用何种方法对列控系统安全因素进行分析在传统研究中并没有涉及,而形式化方法恰好弥补了这一不足,通过选取合适的形式化方法对列控系统进行建模及安全分析已成为目前列控系统安全保障技术的主流研究趋势。本论文以自主化CTCS-3级列控系统轨道电路行车许可校验场景为研究对象,采用两种形式化方法对场景开展研究。首先提出基于时间自动机的建模方法,针对列控系统的实时性,分析场景下列控系统各设备的工作流程,经过合理的抽象简化后,利用时间自动机理论构建了轨道电路行车许可校验场景的时间自动机模型,在UPPAAL模拟器中对各模块交互情况进行仿真,使用验证器验证其安全功能属性和受限活性,证明了此建模方式的有效性,最后结合京沈客专辽宁段试验数据,编制轨道电路行车许可校验场景相关的测试序列,通过自主化CTCS-3级列控系统场景控制器开展仿真测试验证。同时利用UML（Unified Modeling Language,统一建模语言）扩展机制进行轨道电路行车许可校验场景安全分析。针对列控系统的混成性,对轨道电路行车许可校验场景进行分析,根据UML扩展机制对于建模的要求,前期包含UML场景类图以及状态转移图模型构建,对于系统中的状态迁移部分和动态连续过程结合故障扩展模型进一步描述其行为,在列控系统规范要求的基础上建立混成性概要描述文件,后期将已经建立好的模型利用混成自动机模型检验工具进行转换,分析轨道电路行车许可校验场景中可能出现的故障并进行描述,采用故障模型融合算法将PHAVer模型和故障模型融合来描述轨道电路行车许可校验场景中的故障情形和因为故障造成的场景功能影响,利用故障检测器对系统模型开始进行可达集计算,确定涉及系统安全的故障因素组合实现轨道电路行车许可校验场景的安全分析。结果表明,本文提出的方法可以满足轨道电路行车许可校验场景在列控系统需求设计阶段的安全特性要求,为以后列控系统的形式化建模与安全评估提供了参考方法。