Modeling And Verification Of Zone Controller In CBTC With SCADE

With the development of urbanization and increase of population, people are increasingly aware of the advantages of urban railway transportation. Urban railway transportation is building vigorously across the country. Communication-based Train Control System with the advantage of safety, high efficiency and so on is the trend of modern urban railway transportation control system in the future.Zone Controller is the core wayside equipment of CBTC system, its main function is to calculate and assign Movement Authority for trains within its control to ensure the safety of trains on operation. ZC is a safety-critical system, which must meet the need of SIL-4 security level. So in the design and development of ZC system, we must use the most safe method. SCADE (Safety Critical Application Development Environment)provides a complete solution for safety-critical system with model-based development method, so the use of SCADE to develop high safety-critical system like ZC is very appropriate.Train management and MA calculation are main functions of ZC, SCADE is used to build models for the two functions in the thesis. The core of train management function is to manage the status of trains. No matter what status the train is in, ZC must effectively manage trains. MA calculation is the most important function of ZC. In order to calculate MA for trains’safety operation, ZC should communicate with other CBTC subsystems in real time. SCADE safe State machine is used to build model for train management function. For MA calculation function, SCADE builds data flow model.Finally, simulation and verification tools are used to verify train management model and MA calculation model. The use of SCADE simulator is to ensure the correctness of both models. For the completeness of simulation, SCADE MTC (Model Test Coverage) is carried out on the model. In the end, the system’s safety property must be verified with SCADE formal verification to prove the safety of models.