Study on model-based safety verification of Automatic Train Protection system

In railway transportation area, the demand for safety of electronic devices is very high. Automatic train protection (ATP) system is a key equipment of systems for train control. Safety verification is an important issue. Conventionally, safety is ensured by testing manually with a set of test cases after system being integrated. However, testing is a very cost-intensive activity and a complete set of test cases is never achieved. This paper focuses on model-based safety verification approach dedicated to ATP system. We present a formal automaton to express safety, and main safety properties for train protection are studied deeply. And the rigorous semantics of the formal method enable model-based verification mechanisms for system safety. Furthermore, the implementation based on widely used development environment SCADE suite is presented. In conclusion, the strongpoint of the method is discussed.