本论文研究的CTCS-3级列控RBC(Radio Block Center)地面子系统是铁路信号列车控制中一个基于无线通信的实时控车系统,其控车功能是CTCS-3级列控系统功能的核心组成部分。研究的主要内容是基于时间自动机理论,在UPPAAL这种目前最先进的实时系统建模分析验证工具中,对RBC系统进行分析,建模,验证。论文最终对RBC系统控车流程的特性进行了验证,对于保证RBC系统控车流程的安全性、减少系统开发周期及开发成本都有着重要的实际意义。论文完成的主要内容包括绪论、形式化语言及时间自动机理论介绍、RBC系统功能需求分析、RBC系统时间自动机模型建立、在UPPAAL中对RBC系统功能特性的验证:第一章.概述了列车控制系统在国内外的发展与现状,提出了RBC系统形式化建模的目的和意义。第二章.介绍了形式化语言建模的优缺点及阐明了选择时间自动机对RBC系统建模的原因。第三章.通过详细分析RBC系统控车的功能需求,单独建立消息重发流程,根据列车运行要求把RBC控车分为四个流程:列车登录流程,正常控车流程,RBC交接流程,列车注销流程。第四章.介绍了基于时间自动机理论模型检验工具UPPAAL的使用方法。对RBC系统的五个流程以及其他外部设备分别在UPPAAL中建立了时间自动机模型。第五章.通过设置通道和全局变量,构造了时间自动机的积,使用UPPAAL对RBC系统控车流程的时间自动机模型进行了分析验证;使用模拟器,模拟了RBC控制列车运行过程,分析RBC控制列车运行过程中的状态变化;使用验证器,通过快速搜索整个系统的状态空间,验证RBC系统控车流程的活性和正确性等各项特性。