基于通信的列车控制系统可信构造:形式化方法综述

Survey on Formal Method of Trustworthy Construction for Communication-Based Train Control Systems

基于通信的列车控制系统(communication based train control system,简称CBTC)已经成为世界范围内建造轨道交通信号系统的标准制式.CBTC采用更加灵活和精确的列车控制,并提供连续的安全列车间隔保证和超速防护,在很大程度上提高了轨道交通运输的效率和安全性.尽管CBTC能够精确地实施实时控制,但由于CBTC涉及计算、通信与控制这3个方面的实时协同,系统设计与实现异常复杂.由设计缺陷而导致严重的灾难、事故和损失屡见不鲜.作为一个典型的安全攸关系统,如何保证CBTC的可信构造已成为领域研发人员关注的焦点与面临的最大挑战.鉴于在软硬件领域的成功经验,形式化方法目前已被公认为是保障CBTC可信性的一种有效方案.围绕CBTC的可信构造,从其生命周期的3个重要阶段,即系统需求分析、设计建模与底层实现入手,针对CBTC在可信方面的典型特征,梳理分析了CBTC系统在可信构造方面面临的挑战、国内外研究现状和发展趋势,全面介绍了形式化方法在CBTC可信构造中扮演的角色.

Communication-based train control system （CBTC） has become the mainstream infrastructure for the railway signal systems around the world. Unlike traditional track circuit-based railway control systems, CBTC adopts a more flexible and accurate control mechanism to provide uninterrupted services to enable guarantee safeguard between adjacent trains and protection for over-speeding. Therefore, CBTC significantly improves the efficiency and safety of train-based transportation. Although CBTC can accurately conduct real-time control, its design and implementation are extremely complex due to the integration of heterogeneous computation, communication and control components. Consequently, breakdowns caused by CBTC design flaws are inevitable. Therefore, how to guarantee the trustworthiness of CBTC, as for any typical safety-critical system, becomes a big challenge for researchers and practitioners. Due to the huge success in both hardware and software domains, formal methods are now considered as a promising means for trustworthy construction of CBTC systems. This article surveys the three most important stages during the trustworthy construction of CBTC systems, i.e., requirement analysis, design modeling, and bottom-level implementation. It not only comprehensively presents the important roles of the state-of-the-art formal methods and tools during the trustworthy CBTC construction, but also introduces the development trends as well as technical challenges for future CBTC.