Modeling Analysis And Verification Of Temporary Speed Restriction Server In High Speed Railway Train Control System Based On Timed Automata

The temporary speed restriction system is one of the core components of high speed railway train control system,and the workflow of temporary speed restriction is strictly according to the technical specifications of train control system in the passenger dedicated line.In the technical specifications,the temporary speed restriction is divided into the planned speed restriction and the sudden speed restriction,it has strict time logical relation and time constraint characteristics.The formulation and implementation of technical specifications have some human interference,in order to ensure the safety and efficiency of railway system operation,it is necessary to optimize the technical specifications.The temporary speed restriction system is the core of the high speed railway train control system and its safety and bounded liveness are limited by the operational scenarios.Therefore,the formal analysis and modeling description of the system have been used to analysing the flow of system,the occurrence of events and the logical time relationship,verified the logical safety and temporal constraints of the system to meet the requirements of the high speed train control system.Therefore,it is found that the ambiguity of the definition of the temporary speed restriction system and the defects existing in the system,provided a theoretical basis for the subsequent verification of the temporary speed restriction system optimization and deep development.In this thesis,through the analysis of temporary speed restriction to check and feedback execution of basic operation process,it combines with the interactive relationship and interactive mode between the information,and it uses the timed automata theory can build timed automata network models of the three parts: no cross border temporary speed restriction timed automata model,cross border temporary speed restriction timed automata model,timed automata model of TSRS switch and RBC switch overlap region.The timed automata network models of the three different special situations describe the interaction process of the temporary speed restriction command,according to the requirements of real-time and reachability,with different time parameters are set up.According to the specification of the timed automata model and the requirements of technical specifications,the formal BNF grammars have been used to verify the timed automata models in different scenarios.The formal BNF grammar is entered into the verification tool UPPAAL to verify the system's security and limited activity.At the same time,it is finded out the formal BNF grammar which does not meet the requirements of the bounded liveness of the temporary speed restriction system,and analysed the time constraints and give the solution.The results show that the system can meet the security requirements and the limitation of the time parameters in the bounded liveness pointing out the deficiency of the temporary speed restriction system.