Content area
Full text
Introduction
With the rapidly growing of passenger flow in big city, communication-based train control (CBTC) system is believed to be the chief choice for urban railway transportation system. As an emerging new technology, CBTC overcomes the fundamental limitations of conventional track circuit-based railway signal systems and employs continuous, high capacity, bidirectional train-to-wayside data communications to realize high-resolution train location determination. Therefore, train-borne and wayside processors are capable of permitting more effective utilization of the transit infrastructure and implementing a series of vital functions.[1],[2] Taking reliability, availability, maintainability, and safety into consideration, 2 × 2-out-of-2 safety computers are adopted as hardware platforms by more and more safety-critical subsystems in CBTC such as zone controller (ZC) subsystem, data storage unit (DSU) subsystem, computer interlocking (CI) subsystem, and so on.
To copy with the increasingly exacting performance demands in real-time control system,[3]-[6] the architecture and functions of safety computer platform are becoming more and more complex. As a result, the task of verifying that these real-time applications are able to satisfy their timing requirements is more critical and difficult today than ever before. It is believed that analyzing and verifying system performance based on design model is a principal means to ensure the security and reliability of the real-time system.[7] In contrast to classical software engineering measures, model-based development (MBD) is a novel, promising method. MBD supports accurate definition of the system requirements and verification of the designed model in which process formal methods are commonly adopted. Formal methods are mathematics-based techniques, often supported by reasoning tools, which offer a rigorous and effective way to model, design, and analyze computer systems. Rodriguez-Navas and Proenza[8] discussed how computer clocks might influence the temporal behavior of a distributed application and systematically validated the modeling pattern for each type of computer clock. Nemeth and Bartha[9] detailed a formal verification approach for safety procedure of a nuclear power plant written in function block diagram (FBD) language. The approach is based on the Colored Petri net (CPN) representation and a pre-developed library of CPN subnets to represent the FBD specification in an identical structural way. Mokadem et al.[10] introduced a framework of modeling and verification of a particular timed multi-task programmable logic controller, but this model...