Modeling and Verification of Train Control System Level Transition Based on Timed Automata
With the development of train control system,CTCS-3 and CTCS-2 train control systems are mainly used in China's existing railway lines.Level transition plays an important role in the process of train operation control,and the correctness of its function is directly related to the safety of the train control sys-tem.In this paper,the timed automata modeling method is used to analyze the functional and real-time re-quirements of the level conversion scenario according to the requirements specification of the overall basic scheme of CTCS-3 train control system.The functional characteristics and time constraints in the conversion process of CTCS-3 and CTCS-2 train control systems are described.The level conversion scenario is modeled and simulated,and the correctness of the model is verified by formal verification.
train control systemlevel conversionUPPAAL modellingtimed automata
万方数据
维普
