The Formalized Description And Verification Of The Intelligent High-Speed Train RBC Handover Protocol

There is no doubt that the train has brought great conveniences to our life, as it is fastoperated and the network covers most areas of the country. However, people are paying moreattention to the safety and efficiency of the train transportation now. To improve the train’sperformance becomes the core target regarding this field. According to the actual conditions,the future development plan and different kinds of railway lines, China has established ChinaTrain Control System (CTCS), in which Radio Block Center (RBC) is one of the core parts ofits ground sub-system. The function of the RBC is to control movement authorities andintervals of the trains. The RBC handover protocol is one of the factors affecting theefficiency and safety of the train.Compared with other methodologies, Colored Petri Net has a better performance in theresearch and analysis of RBC handover protocol.Compared with other methodologies,Colored Petri Net has a better performance in the research and analysis of RBC handoverprotocol.The other one is Colored Petri Net has a reliable and proven simulation tool, theCPN tools to establish, simulate and analyze CPN models. The CPN tools has acomprehensive function in timing simulating, function analyzing and state space analyzing.Firstly, the paper analyzes the RBC handover protocol through FOCPN. The principle ofthis methodology is to set up formalized models separately for the two cases in the RBChandover process. Thus, the modeling process is simplified, and it is convenient to monitordifferent situations in the handover process. Then the model will be put into the CPN Toolsfor detection and simulation, to draw the conclusion. It is proved that FOCPN can verify theparticularities in the RBC handover and the feasibility to adopt this methodology in the RBChandover field.Secondly, the paper uses timing Colored Petri Net to formalize and analyze the RBChandover protocol. The timing models of the handover with one vehicle station and thehandover with two vehicle stations are set up separately by CPN Tools. Then comparisonsbetween two different cases are made and analyzed to draw the conclusion. The conclusion isit is faster and less time consuming when the handover is made with one vehicle station thanwith two vehicle stations. The result can be used to improve and maintain the RBC handovervehicle stations, and to expedite the repair speed.