Formal Verification Of Safety Computer Platform In CBTC System Based On Timed Automata Model

In many industrial fields, the running foundation of the computer control system must be highly reliable, highly available and highly safe. Safety computer systems are commonly used in military, aerospace, industrial control, banking, telecommunications and other Safety-Critical areas in order to avoid a major accident caused by a computer failure.CBTC(Communications-Based Train Control) system is the development trend of the world's train operation control system, and the major developed countries have developed their own CBTC system. In the CBTC system, ZC (Zone Controller) and DSU (Data Storage Unit) are the main components of the ground-based regional control center. All the VOBC (Vehicle On-Board Controller) of the train in the domain of ZC sent the train location and speed to the ZC application program which runs in the safety computer. After the safety calculation, MA (Movement Authorization) is sent to the VOBC to control the train to run next step. And the DSU subsystem includes all the data and configuration files of the other train control subsystem. Moreover, its application software also needs to run on the platform of safety computer.Using the 2×2-out-of-2 redundant structure safety computer platform is an important solution to improve the system's security and reliability. The safety computer platform of the CBTC trains control system uses the 2×2-out-of-2 structure, and it's a real-time system taking the time factor into account in the control process. The structure of the safety computer system is analyzed and the function of the system is extracted. The timed automata network model of the system is built using the validation tool UPPAAL based on the theory of timed automata. Then the simulation is carried out, and the function, real-time and safety properties of the system is validated.