摘要
The zone control subsystem is a real-time control system,which requests the correctness of the control process.Train tracing scene is an important function of the zone controller(ZC)in the communication based train control(CBTC)system.In the process of deep development and design,to ensure the safety of the system,the system needs to be modeled,simulated and verified to discover the system design flaws.Unified modeling language(UML)is combined with timed automata,and timed automata network models of train-filter and train tracing demarcation-point are established.At the same time,the verification tool of UPPAAL is applied to simulate the system,and verify the requirements of performance and function of system.The results show that the function of train tracing demaraction-point meets the requirements of system safety and limited activity.Therefore,the method is feasible and can be applied to the modeling and verification of other scenes of train control system.
