CTCS(Chinese Train Control System,中国列车控制系统)是我国铁路当中控制列车安全运行,提高列车行车效率的重要装备。RBC(Radio Block Center,无线闭塞中心)是CTCS-3级列控系统的重要组成部分,RBC切换是影响列车安全高效运行的重要环节。列控系统是一种复杂的安全苛求系统,无论是在标准和规范的制定过程当中,或是在系统的开发和设计阶段,都不可避免的会存在着一些系统的漏洞或安全隐患。因此,使用形式化方法对RBC切换协议进行建模与验证是十分必要的。现阶段所使用的形式化验证方法较大部分都基于模型检验,基于定理证明的形式化方法由于能够描述具有无限状态空间的系统,相比之下更适合应用于结构愈加复杂的列控系统,目前所使用的基于定理证明的形式化方法都只针对了列控系统中的某一种特性,很难全面的描述和验证系统。因此,本文采用Timed RAISE(Timed Rigorous Approach to Industrial Software Engineering,工业软件工程的严格方法)的形式化方法,对于CTCS-3级列控系统规范中的RBC切换协议进行建模,对系统模型的正确性和实时性进行验证。首先,对Timed RAISE方法进行了介绍,通过一个具体的实例,描述了RSL(RAISE Specification Language,RAISE标准语言)语言的基本概念并说明了使用RSL语言进行建模与验证的方法,分析说明了在模型验证当中所使用的推理规则。其次,对RBC切换流程进行了分析,根据设备之间信息传递的过程,建立了交互信息图。使用域的方法建立了RBC切换的域模型,在域模型中,将RBC切换整个连续的过程转化为在时间上离散的过程,构建了状态转移图。结合交互信息图中对于信息交互过程的描述,使用RSL语言对状态转移图进行了形式化描述,建立了RBC切换协议的RSL模型。最后,对RBC切换协议的正确性要求和时间约束条件进行了分析,使用RSL语言对切换协议的正确性和实时性进行了描述,使用推理规则结合建立的RSL模型进行推理验证,得到了验证结果。结果表明RBC切换协议满足规范标准对正确性和实时性的要求,将验证结果进行比较分析,说明了该方法具有通用性,同时给出了对切换协议的合理化建议。