The train control system is the heart of Chinese high-speed railways, which is a core technology to ensure safe operation as well as high throughput of trains. The correctness of the train control system is closely related to people's life and property. How to guarantee the correctness of train control system is a grand challenge in both software engineering and control theory. Recently, a group of Chinese researchers proposed an approach to verify the correctness of train control system by combining simulation and formal verification. This work is undertaken jointly by the research group led by Prof. Zhan NaiJun from Institute of Software, Chinese Academy of Sciences and the research group led by Prof. Tang Tao from Beijing Jiaotong University.

In computer science, formal methods are the techniques for specifying, developing and verifying software and hardware systems based on rigorous mathematical theories. Due to the successful application of formal methods to real-world industrial problems, it has become an agreement that safety-critical systems like train control system should be developed using formal methods. However, due to the increasing complexity of the software and hardware in train control system, it becomes extremely difficult, even impossible to pursue formal verification on train control system directly. Additionally, on one hand, it is very hard for experts from train domain to apply formal methods, as it usually requires solid mathematical background; on the other hand, experts from formal method community lack the domain knowledge on train control system. As a result, it is challenging for either of the two sides to complete the work independently.

The experts on formal methods from Institute of Software Chinese Academy of Sciences and the experts on train control system from Beijing Jiaotong University cooperate on this issue, and recently, they propose an effective method on modeling and verification of train control system. The basic idea is as follows: firstly, it applies the graphical environment Simulink/Stateflow, which is easy to follow by train control domain-specific experts, to model train control system, and then simulation can be performed on the model, till the model meets the expectation of the domain-specific experts, or otherwise, some errors or inconsistency are found through the simulation; secondly, as a remedy of inherent incompleteness of simulation, the Simulink/Stateflow graphical model is transformed to a formal Hybrid CSP model using an automatic translator; finally, whether the formal Hybrid CSP model satisfies some desired properties is verified by using a theorem prover for Hybrid Hoare Logic developed by Institute of Software, Chinese Academy of Sciences. In summary, this method provides a seamless integration of practical engineering method and formal methods.

By applying the above proposed method, they model, simulate and verify some basic scenarios and their combinations in the requirement specification of Chinese high-speed train control system, including Movement Authority, Level Upgrade, Mode Conversion and their combinations. The experiments reveal that abnormal stops and/or failures of level transition may occur in several combined scenarios.

This approach advances the state of the art in the verification of train control system, which provides an effective way to guarantee the coherence, consistency and unambiguity of the requirement specification of train control system. In addition, it is of great significance for designing the next generation of train control system in future. (Phys.org)