Modeling And Verification Of Movement Authority Of CBTC Based On SCADE

The rapid development of social economy has promoted the construction process of urban rail transit in China,and the CBTC(Communication-Based Train Control System)is widely used in urban rail transit construction with its advantages such as efficiency,reliability and safety.In urban rail transit,the CBTC system is used to provide a MA(movement authority)for each communication train to ensure the safety of trains on operation.As the wayside equipment of CBTC system,Zone Controller plays an important role in calculating and assigning movement authority for trains.In view of the high security requirements of ZC systems,this paper uses SCADE(Safety Critical Application Development Environment)to model and verify the calculation of MA,which is the core function of the Zone Controller,so that the system can meet the requirements of the safety-critical system.This paper uses the SCADE data flow diagram to establish train operation management model in the process of train operation,including train login,Train information update and train logout management functions,which could supervise and keep records of the change of train information within the jurisdiction of ZC.Then according to the calculation principle of MA,the paper analyzes the different situations of single train running and train tracing,building MA calculation function by SCADE data flow model.Next,SCADE data flow model and safe State machine are used to model the main operation scenes of the train on the basis of the different requirements of MA in different scenes of CBTC zone.Finally,the simulation of the typical operation scenes of the train was done with simulator which is provided by SCADE.The system's safety property must be verified with SCADE formal verification to prove the safety of MA calculation model.The result shows that the designed model satisfies the correctness and safety of the function.