Formal Modeling and Verification Methods for the System Requirement Specifications of Train Control Systems: A Survey

The system requirement specifications (SRSs) of the train control system (TCS) are the starting point and foundation of system design and development. Defects in the SRSs will bring great risk to the success of railway engineering projects. Therefore, formal modeling and verification methods are introduced to ensure the correctness of TCS. However, there is a huge gap between the formal computer executable model and the SRSs of TCS described in natural language. To solve this problem, a complete conversion process of ‘TCS requirement specification <inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"> <tex-math notation="LaTeX">$\rightarrow $ </tex-math></inline-formula> semi-formal models (UML/SysML) <inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"> <tex-math notation="LaTeX">$\rightarrow $ </tex-math></inline-formula> formal models (safety verification model and reliability evaluation model)’ should be created to ensure full coverage and consistency of semi-formal models and formal models to the SRSs of TCS. With the continuous development of wireless communication, artificial intelligence, and control technology, the future advanced TCS is developing towards a more intelligent and autonomous direction. Online safety monitoring and operational state-based maintenance approaches are critical technologies for developing the future advanced TCS. However, the traditional model-checking approach is time-consuming and susceptible to state space explosion problems. To reduce the difficulty of online safety monitoring and reliability evaluation, machine learning algorithms should be combined with the traditional model checking approaches to improve the verification efficiency during train operation. In this paper, we discussed various formal modeling and safety verification methods for the SRSs of TCS and pointed out the above development directions for the advanced TCS.