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

摘要：

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

关键词：基于通信的列车控制系统、安全攸关、可信构造、形式化方法

所属期刊栏目：28

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金91418203,61672230,61402178;上海市青年科技英才扬帆计划14YF1404300National Natural Science Foundation of China91418203,61672230,61402178;Yangfan Projet for Youth Scientist of Shanghai Science and Technology Committee14YF1404300

在线出版日期：2017-06-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共21页

页码：1183-1203