Modeling And Verification Of CBTC Interlocking Based On Scade

The urban rail transit is becoming the best way to solve the traffic problems for its advantages of high efficiency, large volume and energy-saving. CBTC (Communication-based Train Control) system transmits large capacity of information between train and ground through wireless communication, which is widely used in the urban rail transit for its safety, flexibility and high efficiency.CBI (Computer-based Interlocking) is a key subsystem of the CBTC system, which monitors and controls wayside equipment such as switch, section and signal to preset a route, monitor procedure and so on. As a safety-critical system, the CBI system needs to improve its safety constantly to satisfy the development of urban rail transit. The traditional software design and test methods have been unable to meet the safety requirements of the complex interlocking logic and its fail-safety feature. In recent years, model-based software development is gradually accepted in safety-critical systems. SCADE (Safety-Critical Application Development Environment) is dedicated to the development of embedded software with high safety requirements, which provides a built-in simulator and formal design verifier to ensure the safety and functionality of the software. This paper analyzed the CBI logic based on SCADE. First, the logic models are established with data flow, and then tested their correctness by simulating; finally, the formal verification method is used to verify their safety properties. The main work of this paper includes:(1) Introducing the CBTC system and its composition.(2) Analyzing the functions, logic and information interacted with other subsystems of interlocking subsystem based on CBTC.(3) Taking the route setting for example, analyzed the interlocking functional requirements, which is described specified in three parts:the switch module, the route module and the signal module.(4) Researching the theoretical basis, modeling methods and safety guard mechanism of SCADE, including data flow, simulation and formal verification methods.(5) Establishing the interlocking logic model in SCADE with data flow. The SCADE simulator is used to test the correctness of the models, and the SCADE design verifier is used to verify the safety properties.