Modeling Analysis And Implementation Of RBC Handover Based On Timed Automata

At present,China's high-speed railway operating mileage has exceeded two-thirds of the global high-speed railway mileage and the maximum operating speed of high-speed rail is 350km/h.With the increase of high-speed rail mileage and speed,the requirements for the safety and stability of each subsystem of the CTCS-3 train control system are becoming more and more strict.RBC Handover is one of the main operational scenarios of the C3 train control system and one of the main functions of the ground core equipment RBC(Radio Block Center).The time consumed by the RBC Handover process and the probability of successful handover are related to the train operation efficiency and train safety.It is of great significance to study and analyze the RBC Handover.This paper takes RBC Handover as the research object,and uses the time automata theory and modeling tools to construct and verify the formal hierarchical model of RBC Handover process.The process of information exchange between takeover RBC,handover RBC,on-board equipment and balises under GSM-R network communication is simulated,including periodic and aperiodic wireless message transmission and reception.The influence of different message retransmission interval time on the delay of aperiodic messages and the distribution probability of transmission success is analyzed.For different network delay cases,the handover time and the probability of successful handover of the two RBC Handover strategies are compared and analyzed.Based on the above formalized model construction and verification analysis,the design and development of the RBC Handover simulation system is completed.The main work of this paper includes the following points.Firstly,CTCS-3 and RBC Handover are summarized and the cases of formalized methods applied to the train control system at home and abroad are analyzed.The comparative analysis of these formal methods shows that the timed automata theory is most suitable for RBC Handover.And then describe the timed automata theory of formal methods used in this paper and an overview of the model tool UPPAAL.Secondly,the scene overview and strategy analysis of RBC Handover are carried out.RBC Handover is built according to the bottom layer,the middle layer and the top layer.The bottom layer is the GSM-R network transmission fault model,the middle layer is the train-ground wireless message model,including the periodic message and the aperiodic message model and the top layer is the timed automatic subnetwork model composed of the handover RBC model,the takeover RBC model,the on-borad equipment model and the balises model.The three-layer model together constitute a whole timed automaton network model based on two RBC Handover strategies of single and dual MT.Next,the function and performance of the model are verified by the BNF method,including logic,activity,accessibility,probability characteristics,and time characteristics.On the basis of the correct model,the frequency of fault occurrence,the success rate of periodic message transmission,the effect of different message retransmission interval time on message delay and transmission success rate are analyzed.Comparison of handover time and handover success rate of different strategies under different network quality.Finally,based on the model and verification analysis,relying on the Beijing-Shanghai high-speed rail simulation experiment platform,using C#language,MySQL database and other technologies,the development and design of the RBC Handover simulation system is completed.The joint debugging test is performed on the experimental platform and compared the handover time between the two strategies.The model and RBC Handover simulation system in this paper can be applied to theoretical research,engineering design and teaching.