随着"一带一路"战略的推进以及我国中东部地区铁路网的不断完善,西部地区将迎来铁路发展的黄金时期。CTCS-LDL(Chinese Train Control System-Low Density Lines)级列控系统是针对我国西部地区低密度线路运营需求而研发的新型列控系统,目前该系统处于理论探索阶段。为降低运营成本,减少或免于地面设备维护,CTCS-LDL级列控系统使用GNSS技术实现列车定位及完整性检查,地面不设区间轨道电路和信号机,采用虚拟闭塞方式实现列车追踪,这样对地面设备的安全性和可靠性提出了更高的要求。无线闭塞中心(RBC)是CTCS-LDL级列控系统的地面核心设备,主要通过与车载及地面其他设备间的信息交互,实现虚拟轨道占用检查与区间闭塞管理,完成行车控制,因此设计合理的RBC信息控制流程是保证西部铁路列控系统安全行车的基础。通过分析我国低密度线路列控系统的运营需求,本论文将RBC信息控制流程分为地面信息控制流程与控车流程,对其进行设计、建模与验证。论文完成的主要工作如下:首先,通过比较基于 UML 的 COMET(Collaborative Object Modeling and Architectural Design Method)建模方法与基于时间自动机理论的形式化建模方法的优缺点,将二者结合,提出针对RBC的COMET软件建模与验证方法,该方法涵盖了软件开发周期中需求分析、软件建模、模型验证、架构设计、软件编码这一集成化过程。然后,对RBC系统进行功能需求分析,设计系统总体结构模型,将RBC信息控制流程分为地面信息控制流程和控车流程。地面信息控制流程包括轨道占用识别、区间信号点灯和区间改方;控车流程根据运行场景主要分为设备启动、列车注册、正常行车、列车注销、调车、RBC切换等。对上述流程进行详细设计,并建立COMET动态交互模型,再通过转换算法将其转换为时间自动机网络模型。结合RBC系统的功能需求,利用模型验证工具UPPAAL对建立的模型进行仿真,并从逻辑功能、时序功能和安全性的角度对模型进行分析验证。最后,根据建立的RBC信息控制模型,采用COMET分层抽象的软件体系架构,进行仿真软件设计并完成软件开发。通过实验室仿真联调,验证了本文设计的CTCS-LDL级列控系统中RBC信息控制流程的正确性和合理性。