Study on formal modeling and verification of safety computer platform

Abstract

With the development of automatic control and communication technology, communication-based train control system is adopted by more and more urban mass transit system to automatically supervise the train speed to follow a desired trajectory. Taking reliability, availability, maintainability, and safety into consideration, 2 × 2-out-of-2 safety computer platform is usually utilized as the hardware platform of safety-critical subsystem in communication-based train control. To enhance the safety integrity level of safety computer platform, safety-related logics have to be verified before integrating them into practical systems. Therefore, a significant problem of developing safety computer platform is how to guarantee that system behaviors will satisfy the function requirements as well as responding to external events and processes within the limit of right time. Based on the qualitative and quantitative analysis of function and timing characteristics, this article introduces a formal modeling and verification approach for this real-time system. In the proposed method, timed automata network model for 2 × 2-out-of-2 safety computer platform is built, and system requirements are specified and formalized as computation tree logic properties which can be verified by UPPAAL model checker.