列车运行控制系统(简称“列控系统”)是保证列车安全、高效运行的自动化系统。列控系统具有复杂的运营场景功能以及控制模式(如CTCS-3级列控系统含有14个运营场景和9种控制模式),如何保证列控系统在复杂运营场景下(尤其是不同运营场景组合形成复杂场景)功能的正确性显得尤为重要。本文从场景分析方法入手,结合Simulink/Stateflow和时间自动机理论,提出了一种研究复杂场景下列控系统功能正确性的验证方法。(1)首先,分析了高速铁路CTCS-3级列控系统典型的运营场景功能。结合场景分析方法,研究了运营场景之间的关系和运营场景内部子系统之间的交互流程;(2)其次,研究了基于时间自动机理论的运营场景下列控系统建模与验证方法。通过建立典型的等级转换(CTCS-2级至CTCS-3级)和模式转换(FS模式至OS模式)运营场景下CTCS-3级列控系统的时间自动机模型,根据相关运营场景的控制时序流,分析了单一运营场景下列控系统功能的正确性；(3)再次,研究了基于Simulink/Stateflow的复杂运营场景下列控系统建模方法。提出了列控系统运营场景之间的组合规则,建立了基于Simulink/Stateflow的复杂场景下CTCS-3级列控系统仿真模型。以列控系统等级转换和模式转换叠加的复杂运营场景为例,按照等级转换和模式转换运营场景的组合规则,得到了列控系统该复杂场景下的交互流程,并进行了仿真分析；(4)最后,针对复杂运营场景下列控系统功能逻辑进行了修改和验证。论文分别从仿真和形式化两种方法入手,针对修改后的复杂运营场景下列控系统功能逻辑进行了验证分析。首先,针对该修改后的复杂运营场景下列控系统的Simulink/Stateflow模型进行了仿真分析,结论表明列车能够正常运行；其次,针对该复杂运营场景下列控系统建立了时间自动机模型,通过对列车正常运行属性的可达性分析,证明了列控系统在该修改后的复杂运营场景中功能的正确性。