无线闭塞中心(RBC)是CTCS-3级列控系统的地面核心系统,主要实现行车许可的下达与列车间隔控制。RBC切换功能是RBC系统的关键功能之一,是影响CTCS-3级列控系统的控制精度、效率和可靠性、安全性的重要因素。本文分析了RBC切换的功能需求,设计了RBC切换的流程并对RBC切换功能进行模块划分;在此基础上,引入有色Petri网建立RBC切换功能的顶层模型与各子模块模型,并验证和分析了模型的功能和性能。首先,研究了RBC系统的当前研究现状,依据CTCS-3级列控系统划分,得出RBC系统在CTCS-3级列控系统中的重要性和研究的迫切性,分析了RBC切换在RBC系统中的重要地位。其次,根据安全苛求系统的设计要求,提出RBC切换功能的“V”字型软件开发框架,分析了RBC切换的功能需求,设计了RBC切换功能的软件流程;并依据该需求,将RBC切换功能划分成不同功能的子模块;根据各子模块功能,归纳出切换过程中的重要信息。再次,引入有色Petri网对RBC切换进行形式化建模。依据有色Petri网的层次化建模方法,首先建立了RBC系统的CPN模型;继而针对两种不同的RBC切换策略,分别建立不同策略下系统的顶层模型;并根据该策略的顶层模型和功能需求,按照切换功能的模块划分,建立了RBC切换各子模块的完整模型;与此同时,结合RBC切换过程的重要信息,建立了RBC的赋时切换模型。最后,将CPN的仿真分析与状态空间分析方法应用于所设计的RBC切换模型的验证中。以状态空间报告中的内容为依据,参照CPN的动态属性的定义,选取车载装备2部车载电台切换的关键模型,验证该模型的功能并分析了RBC切换在不同的网络质量下的成功率;并从通信延时的角度,讨论了两种切换策略的差异,提出该设计方案的合理化建议。