MODELING AND VERIFICATION OF CROSS-BORDER TEMPORARY SPEED RESTRICTION FOR HIGH SPEED RAILWAY TRAIN CONTROL SYSTEM BASED ONTIMED AUTOMATA

摘要

Temporary Speed Restriction Server (TSRS) is an important part of the High Speed Train Control System, and it not only needs to check the temporary speed limit orders issued by CTC, but also needs to exchange information frequently with temporary speed restriction server of adjacent dispatch stations. For this reason, TSRS has higher requirements for security and real-time property. In order to meet the real-time requirements, timed automata sub-models of the system was established for the working process of Cross-Border Temporary Speed Restriction, and the whole timed automata network models are established through parallel composition of the sub-models. The BNF grammar was used to describe the properties of the Cross-Border Temporary Speed Restriction. Server, and the verification tool of UPPAAL is used to simulate models. And the safety and bounded liveness properties of the system in the interaction process was verified in the verifier.