Study on modeling and verification of CBTC interlocking system

In CBTC (Communications Based Train Control) system, interlocking is considered to be one of the most fundamental system which features in logic complexity and high safety demand. Traditionally, the development and verification of interlocking system is entirely a manual process which relies too much on designers´ experience and some corner-case bugs may not be revealed. In order to solve these problems, our emphasis is paid on formal modeling and model-based verification. This paper introduces an innovative modeling approach to construct system model, express main safety properties, and execute formally verification using SCADE. This method is proven to be helpful for improving the quality and efficiency of interlocking software in practice.