基于有色Petri网的CTCS-3级列控系统RBC切换的建模与形式化分析

在CTCS-3级列控系统中,车载设备在执行RBC切换过程中所用时间的长短和切换成功概率的大小,严重影响着列车的运行效率。本文利用有色Petri网对车载设备进行RBC切换的两种方式分别建模,模型中引入GSM-R故障模型和非周期消息模型,模拟在GSM-R网络中消息的传输过程和重发机制。研究结果表明:基于两部车载电台的RBC切换方式比基于一部车载电台的RBC切换方式所用时间更少,效率更高。列车速度、消息重发时间间隔都会影响列车执行RBC切换的时间。消息重发时间间隔和RBC重叠范围又会影响车载设备进行RBC切换的成功概率。

The Modeling and Formal Analysis of RBC Handover for CTCS-3 Train Control System Based on Colored Petri Nets

In the CTCS-3train control system,the time spent in the RBC handover progress and the success rate of RBC handover seriously influence the traffic efficiency.In this paper,two different ways of RBC handover are modeled with the Colored Petri Nets respectively.In order to simulate the transmission process and the retransmission mechanisms of the messages in the GSM-R network,the GSM-R fault model and non-periodic message model are introduced into the two models mentioned above.The analysis proves that the RBC handover based on two MT2takes less time and operates more efficiently than that besed on one MT2.Both the speed of the train and the time interval of message retransmission affect the RBC handover time.Moreover,the time interval of message retransmission and the RBC overlap influence the success rate of RBC handover.