论文部分内容阅读
目前我国高速铁路运营里程已经超过全球高速铁路里程的三分之二,高铁最高运行允许时速为350km/h。随着高铁里程数与速度的提升,对CTCS-3级列控系统各个子系统设备的安全性与稳定性要求越来越严格。RBC切换既是C3列控系统主要运营场景之一,又是地面核心设备RBC(无线闭塞中心)主要功能之一,RBC切换过程所消耗时长与切换成功率,关系到列车运行效率与行车安全,对RBC切换进行研究与分析有重要意义。本文以RBC切换为研究对象,利用时间自动机理论及建模工具对RBC切换过程进行形式化层次模型搭建与验证分析。模拟了在GSM-R网络通信下,接收RBC、移交RBC、列控车载以及应答器组之间的信息交互流程,其中包括了周期性与非周期性车地无线消息的收发。分析了不同消息重发间隔时间对非周期消息的时延及发送成功概率分布的影响,对不同网络时延情况下,两种切换策略的切换时间及切换成功概率进行对比分析。以上述形式化模型构建与验证分析为理论基础,完成对RBC切换仿真系统的设计开发。本文主要工作内容包括以下几点。首先,对列控系统及RBC切换进行了概述,并分析了国内外形式化方法应用于列控系统的案例,对这些形式化方法进行对比分析,得出时间自动机理论最适合对RBC切换进行建模,进而对本文用到的形式化方法时间自动机理论进行描述,以及对模型工具UPPAAL进行概述。其次,对RBC切换进行场景概述和策略分析,将RBC切换按底层、中层及顶层进行模型搭建。底层为GSM-R网络传输故障模型,中层为车地无线消息模型,包括周期性消息及非周期消息模型,顶层为移交RBC模型、接收RBC模型、车载模型及应答器模型组成的的时间自动机子网络模型,三层模型共同构成了基于单、双电台的两种RBC切换策略的时间自动机网络模型。再次,利用BNF方法对模型的功能和性能进行验证,包括逻辑性、活性、可达性、概率特性、时间特性等。在模型正确的基础上,分析了故障发生频率、周期性消息的发送成功率、非周期消息重发间隔时间对消息时延及发送成功率的影响、不同网络质量下不同策略的切换时间与切换成功率对比情况。最后,以模型与验证分析为理论基础,依托京沪高铁仿真实验平台,利用C#语言、MySQL数据库等技术,完成对RBC切换仿真系统的开发设计,并在实验平台上进行联调测试,对比了两种策略下的切换时间。文中的模型与RBC切换仿真系统可应用于理论研究、工程设计与教学中。