CTCS-3级列控系统是铁路信号领域的主要技术设备,它担负着指挥列车运行,保证行车安全和提高运输效率的重要任务。无线闭塞中心(Raid Block Center, RBC)系统是CTCS-3级列控系统地面设备中的核心设备,它是实现安全、高效控车的关键。由于RBC系统作为安全苛求系统(safety critical system),不仅功能复杂,而且实时性要求极高,因此对RBC系统设计的正确性和可靠性提出了更高的要求。然而传统的系统设计方法存在不能及时发现软件错误和隐患的缺陷,本文探索采用基于时间自动机理论的形式化方法对RBC系统的软件进行安全性设计和验证,以期提高RBC系统设计开发的安全、可靠和正确性。对RBC系统的形式化建模与验证的实质就是寻求一个同被研究原型有极密切映象关系的时间自动机模型研究系统。本文在分析既有RBC形式化建模技术及其优缺点的基础上,研究和探索了根据系统规范对RBC系统基于时间自动机理论进行形式化建模和验证。由于RBC系统是一个大型的、功能复杂的实时系统,为了更加直观清晰地描述系统,以CTCS-3级列控系统标准规范为依据,以RBC系统的主要控车运营场景作为切入点,分析各个场景中RBC系统的控车流程,建立了主要功能场景的时间自动机模型,并通过通道和全局变量组建成时间自动机网络模型。然后在UPPAAL工具中对所建模型进行模拟仿真,提取系统的关键功能点,并将其转化为BNF语法中的语句,在UPPAAL验证器中对网络模型的正确性进行验证。利用UPPAAL验证的结果表明,所建基于时间自动机理论和基于规范的RBC系统形式化模型是可行的,也为设计正确可靠RBC系统提供了一条新的途径,具有实际工程应用指导意义。