RBC(Radio Block Center,无线闭塞中心)是CTCS(Chinese Train Control System Level,中国列车控制系统等级)3级列控系统中保障列车安全可靠运行的关键设备,其根据从地面设备收到的信息数据以及通过GSM-R(Global System for Mobile Communications–Railway,全球数字铁路移动通信系统)网络与车载系统进行连续双向的交互信息生成MA(Movement Authority,行车许可)来控制列车可靠行驶,从而保证了列车在运行线路上安全运行。RBC具有苛刻的实时性要求,能否满足此要求直接影响CTCS-3级列控系统安全、可靠、高效和精确地控制列车。保证RBC系统的可靠工作和实时性要求,必须保证指导列控系统设计的需求规范和设计技术规范中不存在任何缺陷,否则都有可能将潜在的风险演变成系统的失效从而导致安全事故的发生。因此,对相应的规范建模验证将成为保证其正确合理的有效手段。本文以CTCS-3列控系统需求规范为背景,采用半形式化方法UML(Unified Modeling Language,统一建模语言)和形式化方法时间自动机相结合的方法,对等级转换和RBC切换两个运营场景进行建模验证,保证RBC控车的实时性和安全性要求。首先,对CTCS-3级列控系统需求规范和设计技术方案中的两个场景过程进行分析,并根据时间特征将各场景划分为若干模块;其次,根据系统实时性和信息动态交互等要求,使用UML中扩展了时间特征的顺序图和定时图对每一个子模块进行建模;再次,利用从UML顺序图到时间自动机的转换规则,将建立的UML顺序图和定时图模型无差别的转化为时间自动机子模型;最后,根据时间自动机积的原理将各独立的时间自动机子模型合并成系统的时间自动机整体网络模型,并采用UPPAAL验证工具对已有模型仿真得到状态迁移图,利用从规范中提炼出的BNF(Backus Normal Form,巴科斯范式)验证语句,逐一验证整体网络模型中系统的实时和安全等性质,最终达到对规范建模验证的目的。UML和时间自动机结合,在对系统规范进行建模验证中,不仅能够准确的表达规范语义,而且能够合理的对系统的性能进行验证,为CTCS-3级列控系统的完善和更高级列控系统的研究和开发提供了参考。