/   Home   /   Newsroom   /   Research News

Progress in Safety Verification of Chinese High-speed Train Control System

Jun 09, 2015     Email"> PrintText Size

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)

Attachment:

(Editor: CHEN Na)

Contact

ZHAN Naijun

State Key Lab. of Computer Science, Institute of Software

Phone:
E-mail: znj@ios.ac.cn

Related Articles

TCSN;train control system;CRRC

Faster Train Control System Gives Chinese Firm Tech Edge

Mar 16, 2016

A faster transmission system developed by stated-owned train maker CRRC has been successfully tested in its trains, giving the firm an edge over rivals in key rail technology. The system, called TCSN, is a proprietary information transmission network developed by the Zhuz...

high speed rail;high speed train

Experience the Rush of High Speed Rail

Feb 08, 2017

This clip shows testing of high speed train technology in the laboratory of the Institute of Mechanics at the Chinese Academy of Sciences in Beijing. The experimental platform is 274 meters long, the world's largest platform of its kind to conduct tests and experiments on...

Contact Us

Copyright © 2002 - 2017 Chinese Academy of Sciences