Failure Analysis of Chinese Train Control System Level 3 Based on Model Checking

摘要

The complexity of railway control system makes some requirement deficiencies hard to find, which results in system failures. It is essential to locate those deficiencies using logs recorded during failure events. In this paper, a model checking based failure analysis approach was proposed and applied to a case of abnormal emergency brake. First, a system model describing the system requirement and an event model depicting the logs were constructed. Next the compositional model was verified through model checking in UPPAAL which then produced a counterexample trace that describes the system behaviour in the failure event. By analysing this trace, an inadequacy was found in the requirement and a modification strategy was brought up which was formally verified to be effective.