列车运行控制系统是控制列车安全、高效运行的关键信号设备。近年来,随着列控技术的发展,系统结构精简、行车间隔缩短和运营成本降低等要求愈发迫切,以车载为核心、车车通信技术为基础的新型列控系统的研究应运而生。以车载为核心的联锁将原有地面集中联锁的功能集成到车载设备,实现不同列车对线路资源和进路的分散独立控制。联锁控制的安全苛求特性,决定了其安全功能的正确实现不可或缺,探索一套有效的建模与验证方法至关重要。论文引入图形化的建模工具Simulink/Stateflow和形式化的Timed Automata(TA)时间自动机理论,构建了一套完整的以车载为核心联锁控制的建模与验证框架,在确定的场景下,先后完成对联锁进路控制的图形化建模仿真和联锁功能的形式化验证。具体工作如下:(1)以城市轨道交通为背景,分析了新型列控系统的功能原理和系统架构,对比了以车载为核心的联锁控制与地面集中联锁在控制结构、资源管理和进路处理方面的异同,对线路资源的划分和调用策略展开介绍,采用场景分析法研究了联锁相关场景(正常场景和异常场景)中各模块间的信息交互情况。(2)提出了基于Simulink/Stateflow的以车载为核心联锁控制的建模方法,通过对以车载为核心联锁的模块化和层次化建模,有效地满足了不同场景下联锁控制建模的要求;围绕联锁控制模型的功能特性验证,提出了Stateflow状态图到TA模型的转换规则,并进行了映射规则的正确性分析。在此基础上,构建了基于Simulink/Stateflow和TA的联锁控制建模与验证框架。(3)分析了联锁控制的静态结构和动态行为,利用Simulink/Stateflow构建了可重组的模块化模型,完成了正常场景(接发车进路、通过进路、追踪运行以及进路冲突)和异常场景(通信中断、OC故障等)层联锁控制的建模及仿真分析,检验了确定场景下联锁控制功能的正确实现。(4)围绕联锁控制模型的验证,以典型的接发车进路场景为例,建立了联锁控制的TA网络模型,并利用BNF验证语句对安全相关的联锁功能、道岔控制功能以及系统模型的活性、实时性进行形式化验证。结论表明在该场景下,以车载为核心的联锁控制满足进路的建立、解锁和道岔控制功能,能够实现进路的安全控制,有效地保证了系统功能实现的正确性。