Modeling And Verification Of Temporary Speed Restriction Of Train Control System

Temporary speed restriction (TSR) refers to the planned speed restriction caused by construction, maintenance and the unexpected speed restriction caused by natural disasters, equipment failures. The TSR is set in relation to transport efficiency and traffic safety. As the train speed gets faster and faster, the security demand of TSR is also increasing. TSR system is an important part of the train control system, is a safety-critical system related to traffic safety and transport efficiency. The workflow of TSR system has strict timing logic, reflecting the precise time constraint characteristics.For these characteristics of the TSR system, it is necessary to carry out real-time analysis of its workflow and describe its properties and behaviors using formal methods modeling. By verifying the logic and time properties of the results and the real-time property of the TSR system, which can found the incompleteness and ambiguity of its specifications, in order to ensure the security of the TSR system, and to provide an important basis for improving the design and development.This paper analyzes the structure of the TSR system, clarifies the relationship of information exchange between devices, combines with its functionality and the operation processes of TSR to indicate the way of information interactive. To establish a TSR-system model using timed automata theory. There are two different scenes of the TSR system, they are TSR in high-speed rail CTC dispatcher boundaries and TSR in CTCS grade transition area. Establishing the automata model individually by considering the different workflows particular of the two scenes. Through the model, the behaviors of the system were accurately described, avoiding specification incompleteness and ambiguity. Extract the required function properties and performance attributes of TSR-system, and give their BNF syntax descriptions. On the basis of the time automa model, use UPPAAL tool to simulate the workflow of the TSR-system, we can get the simulation timing diagram. Then verify the function properties and performance attributes of TSR-system. The verification results confirmed the time, safety and bounded liveness properties of TSR system.