Formal Analysis Of Temporary Speed Restriction Of Chinese Train Control System And Research On Diagnosis Of Anomalies

Since the Ministry of Railways established the Chinese train operation control system in 2002,the domestic train operation control technology has developed rapidly in just over ten years.While people enjoy the convenience brought about by high-speed railways,the safety of train operations has gradually become the focus of research.Temporary speed restriction refers to the speed restriction that has a certain timeliness when encountering unexpected situations such as road construction,equipment failure,etc.in addition to the fixed speed restriction during the course of train operation.The temporary speed restriction command is issued by the dispatch center to the temporary speed restriction server.According to the rank of the train control system,the order is further transmitted to the onvehicle equipment by the train control center or wireless blocking center through the corresponding transmission channel to execute the command in time to ensure the train's travel safely.The structure of the temporary speed restriction system itself is complicated,and information exchanges between devices are frequent.Abnormalities arising from information exchange and failures caused by the device itself will cause the speed restriction command to be invalid.Therefore,it is necessary to analyze the abnormal conditions generated in the temporary speed restriction and use proper methods to diagnose it to improve the safety of the system's early design and the high efficiency of the subsequent maintenance.This thesis focuses on the temporary speed restriction to carry out research on the subject.Firstly,through the analysis of the main components of the temporary speed restriction system,the flow of speed restriction commands,etc.,setting it as a basis for formal analysis.Then,the formal method of time automata is selected,and UPPAAL is used for formal simulation and verification.Based on the information interaction between the automata of each member,the timing simulation of the command operation flow,and the verification of the functional properties and restricted activity of the model are performed.Finally,the internal information interaction and equipment status of the system are selected as objects.From two perspectives,different diagnostic methods are used to analyze the abnormalities generated by the information interaction and the faults generated by the system equipment.Among them,the system-level fault diagnosis method based on graph theory is adopted in the perspective of information interaction.After selecting an appropriate test model,the interaction information is abstracted as test information,related diagnostic methods are designed,correlation calculation is performed based on the test information to figure out the state of the equipment during the test process;The Bayesian network inference method is used at the equipment failure angle,and the fault tree is established with the temporary speed restriction failure as the top event.Through the model conversion to the Bayesian network,the probability diagnosis is used,and the connection tree inference method is used to establish the fault tree.The Bayesian network conducts conditional probability inference and concludes that the fault link is the most likely to cause anomalies.