轨道交通是我国交通体系中的一个重要组成部分,随着轨道交通的日益完善,功能系统日益复杂,安全问题也不断突出。列车运行控制系统作为轨道交通中的一个重要系统,也是集控制、通信、计算和信号于一体的复杂系统。现阶段对列车运行控制系统安全验证的传统测试和验证方法都有其局限性,而运行时验证方法是结合了传统测试和模型检验方法的轻量级形式化方法。它有效降低了对安全苛求的列车运行控制系统安全验证的复杂度,同时提高了验证的效率。目前对运行时验证研究比较多的是线性时序逻辑(LTL),但LTL只能对系统执行的状态序列进行监控,无法描述实时系统的实时时序属性。在国内外运行时验证研究的基础上,论文主要针对运行时验证方法对实时时序属性的验证展开了深入的研究。首先,对运行时验证的基本理论知识进行了深入研究,阐述了运行时验证的特点,了解其在对列控系统安全验证方面的应用,并对运行时验证的两种基本方法进行了详细的分析。其次,对于列控系统这样安全苛求的实时系统,现有的时序逻辑运行时验证算法不能对系统的实时性质进行监控验证,表达能力不足。本文提出了能够描述带有显式时间约束的度量时序逻辑(MTL)和时间命题时序逻辑(TPTL)的重写语义。并在该语义的基础上分别提出了基于MTL和基于TPTL的公式重写型验证监控算法。这两种监控算法丰富了监控需求的表达能力,描述出的时间约束性质能够对实时系统的时间轨迹进行监控,从而克服了 LTL无法对时间轨迹进行监控的不足。最后,为了更加方便的运用本文提出的运行时监控算法对实时系统实时属性进行验证,本文在底层Maude工具的基础上对算法进行封装,开发了可以进行自动化验证的运行时验证工具。为了对轨道交通车载控制器进行验证,开发了可与实验室半实物平台进行数据传输的接口,用以接收列车运行过程中的实际数据。根据系统的高层规范提取列车运行需要满足的监控需求,并运用所开发的工具进行验证和分析。另外,本文还以CTCS-3级列控系统的重要场景为案例进行了具体的运用演示。通过上述案例验证了运行时监控算法的可行性,演示了该工具在列控领域中的具体应用方法。