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

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.