Modelling And Analysis Of Computer Based Interlocking System Based On Safe State Machine

The urban rail transit has becoming a promising solution to the problem of congestion for its advantages of safety and reliability, low pollution, large traffic volume, high speed and little interference by other transportations. The CBTC (Communication-based Train Control) system is an important market tendency of the train control technology, which possesses less wayside equipments, shorter tracking interval, and higher operating efficiency. As a key subsystem of CBTC, the CBI (Computer-based Interlocking) system is a safty critcal system, which needs a high safety and reliability requirements since it affects the safety of trains directly. So there is significance for CBI to ensure its safety and correctness of design and development.SSM (Safe State Machine) is a visual synchronous modeling language with hierarchy, concurrency, preemption and communication mechanism, and due to its clarity, conciseness and good readability, SSM is appropriate for describing the complex logic of safety critical system. The formal theory basis of SSM avoids the flaw of ambiguity of tranditional requirements analysis methods, and owing to the modeling, simulation and formal verification supported by SCADE (Safety Critical Application Development Environment), SSM has well applied in practical engineering application.This paper adopts SSM to model and nanlyze the CBI, and main work includes:(1) the theory basis, features, and configuration mechanism of SSM is analyzed, and its modeling, simulation and formal verification method in SCADE is introduced;(2) the CBI basic structure, interlocking function in CBTC and interaction between CBI and subsystems of CBTC is analyzed, then compared the differences between CBI and the traditional interlocking;(3) the CBI logic is analzed through dividing the CBI into switch, route and signal modules, and the SSM models is established with SCADE, including switch request and lock, route request and check, section lock and signal logic; then the data flow diagram is used to integrate switch, route and signal modules into a complete CBI logic model;(4) the CBI model correctness is checked through SCADE simulation, and then, to ensure CBI safety and correctness, the safety properties is extracted and the formal verification is perfomed using SCADE, which shows that the safety properties are fulfilled.