Formal Modelling and Analysis of RBC Handover Protocol for ETCS Level 2 Using Stochastic Petri Nets
Tao Tang · Journal of the China Railway Society · 2009
The RBC(radio block center) handover protocol is one of the important factors affecting the control-proficiency,transportation ability,reliability and safety of the ETCS system.So the formalism of the qualities of the protocol is of great value to the establishment and improvement of the CTCS Level 3 system.We choose Stochastic Petri Net(SPN) as the formal language to analyze this protocol,which is proved more powerful to give out quantitative results compared with normal simulation methods.The current study has established the failure probability models of the handover procedure with two different train configurations,which captures the channel degradation,GSM-R cell switch and link failure.Besides,the study offers an analysis of the influence of different train velocities and RBC overlap on the successful probability of RBC handover.The study shows that the RBC handover protocol based on double mobile stations,which provides separate communication channels with each RBC during handover,proves to be of greater safety and be less sensitive to the influence of train velocities.