CTCS-3(China Train Control System level 3)级列车控制运行系统是保障我国铁路时速300~350 km客运专线高速列车安全、可靠、高效运行的核心技术之一。然而,对于列车控制运行系统这种实时安全关键系统,仅仅依靠经验和自然语言来制定和描述系统的需求规范会难以避免的存在某些缺陷和不安全因素,并且系统的测试若都以现场跑车为主,也会消耗大量的时间和精力。因此,需要一种技术来验证这种实时系统的特性,从而提高系统的正确性或完善系统的功能。基于严格数学定义的形式化方法,由于其能够简洁、准确的描述系统的规格,并验证系统的特性,因此能够作为系统建模和验证的重要理论方法。而时序逻辑作为一种形式化方法,近些年来已经被广泛的运用于实时系统的建模和验证中。实时建模、仿真及验证语言(Timed Modeling Simulation and Verification Language,TMSVL)是一种基于实时投影时序逻辑(Timed Projection Temporal Logic,TPTL)的实时时序逻辑程序设计语言,它主要用于对实时系统规范的建模、仿真和验证。本文以TMSVL语言作为实时建模、仿真和验证的形式化语言,以我国CTCS-3级列控系统作为建模和验证的对象,提出了一种基于TMSVL语言的CTCS-3级列控系统运营场景形式化建模与验证的方法。文章首先介绍了TPTL和TMSVL的语法和语义,以及其执行平台TMSV(Timed Modeling Simulation and Verification platform,TMSV),然后简单介绍了CTCS-3级列控系统的结构,并以CTCS-3级列控系统的规范文档作为建模的基础,针对CTCS-3系统规范中的一些核心的运营场景,使用TMSVL语言进行建模,使用实时命题投影时序逻辑(Timed Propositional Projection Temporal Logic,TPPTL)语句描述实时性质和安全性质,最终在其建模和验证环境TMSV平台中完成了CTCS-3级列控系统的建模、仿真和验证。