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

• 作者: 周庭梁 孙海英 缪炜恺 陈小红 陈铭松 鲍勇翔
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 基于通信的列车控制系统 安全攸关 可信构造 形式化方法
• 年，卷（期）: 2017,（5）
• 所属期刊栏目: 形式化方法与应用专题
• 页码范围: 1183-1203
• 页数: 21页
• 分类号: TP311
• 字数: 21786字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005217

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	周庭梁		16	68	4.0	8.0