Research On Modeling And Verification Of Train-centric Interlocking Control

Train control system is the key signal equipment to control the safe and efficient operation of trains.In recent years,with the development of train control technology,it is urgent to simplify the system structure,shorten the driving interval and reduce the operation cost.The research of new train control system with on-board equipment as the core and based on train-to-train communication technology emerges at the right moment.Train-centric interlocking integrates the functions of the original ground centralized interlocking into the on-board equipment,and achieves the decentralized and independent control of line resources and routes of different trains.The safety-critical characteristics of interlocking control determine that the correct realization of its security functions is indispensable.It is essential to explore a effective modeling and verification methods.In this paper,the graphical modelling tool Simulink/Stateflow and the formal timed automata(TA)theory are introduced to construct a complete modeling and verification framework for train-centric interlocking control.Under the defined scenario,the graphical modeling simulation and formal verification of train-centric interlocking control are completed successively.The specific work is as follows:(1)Taking urban rail transit as the background,the functional principle and system architecture of the new train control system are analyzed.The similarities and differences in control structure,resource management and route processing between train-centric interlocking and ground centralized interlocking are compared.This paper presents the division and invocation strategy of line resources,and studies the information interaction between modules in interlocking related scenario(normal scenario and abnormal scenario)with scenario analysis method.(2)A modeling method based on Simulink/Stateflow for train-centric interlocking control is proposed.Through modularization and hierarchical modeling of train-centric interlocking,the modeling requirements of interlocking control in different scenarios can be effectively satisfied.According to the verification of the functional characteristics of interlocking control model,the mapping rules from Stateflow diagram to TA model is provided and the preciseness are analyzed additionally.On this basis,a framework for modeling and validating interlocking control behavior utilized Simulink/Stateflow and TA is established.(3)The static structure and dynamic behavior of train-centric interlocking control are discussed,and the reconfigurable modular models are implemented by using Simulink/Stateflow.Modeling and simulation of interlocking control in normal scenario(receiving and departing route,through route,tracking operation and route conflict)and abnormal scenario(communication interruption,OC fault,etc.)layers are completed and verified to determine the correct implementation of interlocking control function in scenarios.(4)Around the verification of interlocking control model,the TA network model is accomplished by taking the typical scenario of receiving and departing route as an example.The security-related interlocking,switch control function and the activity and real-time of system model are formal validated by BNF statement.The results show that the train-centric interlocking control satisfies the functions of route establishment,unlocking and switch control in this scenario.It can realize the safety control of route and effectively ensure the correctness of system function.