中国高速铁路列控系统的形式化分析与验证
摘要
It is essential that the correctness of high-speed train control systems be guaranteed by formal verification because they are safety-critical. However, as these systems become increasingly more complicated, achieving this goal in practice is difficult, and may even be infeasible. On the other hand, it is more convenient to graphically model a complicated system. A graphical model is fairly intuitive, which has resulted in such models being used extensively in industry. Thus, to improve the reliability of a high-speed train control system, constructing a graphical model for the system and then detecting its bugs by simulation should be very effective. In this paper, we first show how to use Simulink/Stateflow to build graphical models for various combined scenarios of Chinese train control systems (CTCS), in which mode conversion and level upgrade take place simultaneously. This modeling approach can be easily adapted to model other scenarios in CTCS by simply modifying the corresponding parameters. Then, we analyze these graphical models via simulations and show that under some circumstances the trains will stop abnormally. Finally, in order to avoid the inherent incompleteness of simulation, we show how to translate these graphical models into formal models given in HCSP-a formal modeling language for hybrid systems that extends CSP-and subsequently formally prove that abnormal stops can happen in many of the cases in one of the combined scenarios. Formal verification of Simulink/Stateflow diagrams complements simulation and improves the reliability of systems being developed.