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

作     者：陈铭松 鲍勇翔 孙海英 缪炜恺 陈小红 周庭梁 CHEN Ming-Song;BAO Yong-Xiang;SUN Hai-Ying;MIAO Wei-Kai;CHEN Xiao-Hong;ZHOU Ting-Liang

作者机构：上海市高可信重点实验室(华东师范大学)上海200062 卡斯柯信号有限公司上海200071 

基　　金：国家自然科学基金(91418203 61672230 61402178) 上海市青年科技英才扬帆计划(14YF1404300)~~ 

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2017年第28卷第5期

页      码：1183-1203页

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

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

学科分类：08[工学] 0835[0835] 0811[工学-水利类] 0812[工学-测绘类] 081202[081202] 

核心收录：

D　O　I：10.13328/j.cnki.jos.005217

馆 藏 号：203230532...