CTCS-3列控系统RBC切换的形式化建模、分析与验证

Formal modeling,analysis and verification of RBC handover for CTCS-3 train control system

针对影响RBC切换质量的列车速度、RBC切换时间等诸因素,以及澄清对RBC交接协议安全性在认识上的一些误区,利用随机Petri网形式化描述工具,建立了CTCS-3列控系统RBC切换模型。通过理论分析和仿真实验,验证了不同速度条件下高速列车越区运行RBC交接协议A、B的可靠性、安全性和合理性。交接协议B作为协议A的冗余措施,由于考虑了RBC切换过程中通信中断时间,从RBC切换成功概率上讲,并不存在安全上的问题,但降低了RBC切换效率,对行车效率有所影响;列车速度进一步提高时,RBC切换的可靠性下降,可考虑适当增加RBC重叠覆盖区域、场强和列车间隔时间裕量。

In order to understand the influence of train speed, RBC handover time, etc. on the quality of RBC handover, and clarify the misunderstanding on the safety of RBC handover protocols, it chosen the stochastic Petri net as the formal descrip- tion tool to establish the RBC handover model of Chinese train control system level 3. By theoretical analysis and simulations, verified the reliability, safety and rationality of RBC handover protocol A, B under the condition of high-speed train running in RBC handover area with different speed. Because the interruption interval had been taken into account by the RBC handover protocol B, as a redundant measure of protocol A, it has no safety problem in terms of the success probability of RBC ban- dover, but the reduction of RBC handover efficiency has a negative impact on the efficiency of train operation. On the other hand, as the train speed increases, the reliability of RBC handover will go down. To keep the reliability meeting with require- ments of the related standards, increasing the overlapping coverage areas between the adjacent RBCs, radio-field strength and the time margin of train headway can be taken into account.