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

来源：软件学报杂志2017年第5期北京时间：

作者：陈铭松,鲍勇翔,孙海英,缪炜恺,陈小红,周庭梁

单位：陈铭松，上海市高可信重点实验室(华东师范大学), 上海 20006211,鲍勇翔，上海市高可信重点实验室(华东师范大学), 上海 20006202,孙海英，上海市高可信重点实验室(华东师范大学), 上海 20006203,缪炜恺，上海市高可信重点实验室(华东师范大学), 上海 20006204,陈小红，上海市高可信重点实验室(华东师范大学), 上海 20006205,周庭梁，卡斯柯信号有限公司, 上海 20007106

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

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

基金资助：国家自然科学基金（91418203，61672230，61402178）；上海市青年科技英才扬帆计划（14YF1404300）