主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第12期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
陈铭松,鲍勇翔,孙海英,缪炜恺,陈小红,周庭梁.基于通信的列车控制系统可信构造:形式化方法综述.软件学报,2017,28(5):1183-1203
基于通信的列车控制系统可信构造:形式化方法综述
Survey on Formal Method of Trustworthy Construction for Communication-Based Train Control Systems
投稿时间:2016-07-29  修订日期:2016-09-25
DOI:10.13328/j.cnki.jos.005217
中文关键词:  基于通信的列车控制系统  安全攸关  可信构造  形式化方法
英文关键词:communication-based train control system  safety-critical  trustworthy construction  formal method
基金项目:国家自然科学基金(91418203,61672230,61402178);上海市青年科技英才扬帆计划(14YF1404300)
作者单位E-mail
陈铭松 上海市高可信重点实验室(华东师范大学), 上海 200062  
鲍勇翔 上海市高可信重点实验室(华东师范大学), 上海 200062  
孙海英 上海市高可信重点实验室(华东师范大学), 上海 200062  
缪炜恺 上海市高可信重点实验室(华东师范大学), 上海 200062  
陈小红 上海市高可信重点实验室(华东师范大学), 上海 200062 xhchen@sei.ecnu.edu.cn 
周庭梁 卡斯柯信号有限公司, 上海 200071  
摘要点击次数: 1423
全文下载次数: 2093
中文摘要:
      基于通信的列车控制系统(communication based train control system,简称CBTC)已经成为世界范围内建造轨道交通信号系统的标准制式.CBTC采用更加灵活和精确的列车控制,并提供连续的安全列车间隔保证和超速防护,在很大程度上提高了轨道交通运输的效率和安全性.尽管CBTC能够精确地实施实时控制,但由于CBTC涉及计算、通信与控制这3个方面的实时协同,系统设计与实现异常复杂.由设计缺陷而导致严重的灾难、事故和损失屡见不鲜.作为一个典型的安全攸关系统,如何保证CBTC的可信构造已成为领域研发人员关注的焦点与面临的最大挑战.鉴于在软硬件领域的成功经验,形式化方法目前已被公认为是保障CBTC可信性的一种有效方案.围绕CBTC的可信构造,从其生命周期的3个重要阶段,即系统需求分析、设计建模与底层实现入手,针对CBTC在可信方面的典型特征,梳理分析了CBTC系统在可信构造方面面临的挑战、国内外研究现状和发展趋势,全面介绍了形式化方法在CBTC可信构造中扮演的角色.
英文摘要:
      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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利