Decomposing Automatic Train Control Verification System with Projection

In recent years, with gradual application of formal verification methods to automatic train control (ATC) systems, the problem of verification failure occurs due to the complexity of the verification system. In order to solve this problem, this paper proposes a safety attribute based projection for the ATC systems. We describe this verification system using Problem Frames approach and define projection operators. By projection, the original verification system is divided into several sub-systems. An experiment is also conducted with data collected from a metro line. The experimental results show that the projection can effectively simplify the system state, and increase the efficiency of formal verification.