基于失效日志的CTCS-3级列控车载子系统需求错误所致的失效致因分析

作     者：韩笑 唐涛 吕继东 尚麟宇 HAN Xiao;TANG Tao;L(U) Jidong;SHANG Linyu

作者机构：北京交通大学轨道交通控制与安全国家重点实验室北京100044 北京交通大学轨道交通运行控制系统国家工程研究中心北京100044 中国铁道科学研究院通信信号研究所北京100081 

出 版 物：《铁道学报》 (Journal of the China Railway Society)

年 卷 期：2017年第39卷第3期

页      面：59-70页

核心收录：

学科分类：12[管理学] 1201[管理学-管理科学与工程(可授管理学、工学学位)] 08[工学] 0802[工学-机械工程] 081201[工学-计算机系统结构] 082302[工学-交通信息工程及控制] 0801[工学-力学（可授工学、理学学位）] 0812[工学-计算机科学与技术（可授工学、理学学位）] 0823[工学-交通运输工程] 

基　　金：国家自然科学基金(61304185 U1434209) 国家重点基础研究发展计划(973计划)(2014CB340703) 中国铁路总公司科技研究开发计划(2014X003-D) 

主　　题：CTCS 车载子系统 失效致因分析 时间自动机 UPPAAL 模型检查 需求错误 

摘      要：CTCS-3级列控系统的复杂性使得某些需求错误难以发现,从而导致系统失效,需要结合失效事件的日志记录反向分析出需求的错误。本文采用基于模型检查的方法,首先利用时间自动机建立CTCS-3级列控车载子系统需求的模型,同时利用失效事件中的记录数据建立描述失效事件过程的事件模型,然后对系统模型和事件模型的组合模型使用UPPAAL工具进行模型检查,验证不通过给出的反例描述了失效事件中系统的行为,对此进行分析可以找到系统需求中的错误并据此对系统进行修改。本文以CTCS-3级列控系统中列车异常紧急制动的真实事件为例,分析了因为需求不充分而导致的系统失效致因,并对解决方案进行了验证。