| With the rapid development of technology of communication, control and computer, urban rail transit has become a great promising part of construction in many countries and cities, of which the computer based interlocking system is a core part and takes an important safety responsibility for the movement of trains.As computer technology is widely applied in CBTC (Communication Based Train Control) interlocking system, the complexity and uncertainly of system has greatly increased, which makes the system safety assurance becomes more difficult.Therefore, a scientific and complete analysis and verification method is needed for the interlocking in the process of design and development. Due to the limitations of incompleteness of the traditional requirements analysis methods, this paper employs a formal method of Timed Automata to model and analyze the CBTC interlocking system to improve its system safety.First, the basic theory of CBTC interlocking is presented, and then the main functional requirements are analyzed. On this basis, the functional modules of route control process of interlocking are divided, and the main route control process of CBTC interlocking system is analyzed.Then, according to the process and sequence of interlocking logic, the functionalities and constraints of which is abstracted, and formal models of switch, route, and signal module in route control process are established based on Timed Automata theory, including switch request, switch correspondence check, switch lock, signal request, route check, section lock and signal open, and then a complete Timed Automata model of the process of CBTC interlocking route control is constructed. Timed logic of interlocking is designed with the clock feature of Timed Automata, and Timed Automata network of CBTC interlocking is established using the channel and global variable mechanism.Finally, a simulation and formal verification of the timed automata network is performed by UPPAAL, and a sequence diagram of route control process is formed, which is used to analyze the communication and states transition between models. The functional requirements, safety requirements and time constraints of the route control process are extracted and described formally using BNF grammar, then verified in UPPAAL verifier, which shows that the expected requirements are fulfilled and the Timed Automata method is feasible for CBTC interlocking analysis. |
