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

Analysis of Requirement-errors-caused Failure of On-board Subsystem of CTCS-3 Train Control System Based on Failure Logs

作　　者：韩笑[1] 唐涛[1] 吕继东[2] 尚麟宇[3] 

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

出　　处：《铁道学报》2017年第3期59-70,共12页Journal of the China Railway Society

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

摘　　要：CTCS-3级列控系统的复杂性使得某些需求错误难以发现,从而导致系统失效,需要结合失效事件的日志记录反向分析出需求的错误。本文采用基于模型检查的方法,首先利用时间自动机建立CTCS-3级列控车载子系统需求的模型,同时利用失效事件中的记录数据建立描述失效事件过程的事件模型,然后对系统模型和事件模型的组合模型使用UPPAAL工具进行模型检查,验证不通过给出的反例描述了失效事件中系统的行为,对此进行分析可以找到系统需求中的错误并据此对系统进行修改。本文以CTCS-3级列控系统中列车异常紧急制动的真实事件为例,分析了因为需求不充分而导致的系统失效致因,并对解决方案进行了验证。The complexity of CTCS-3train control system makes some requirement errors hard to find,resulting in system failures.Those errors can be located by using logs recorded during system failure.With a model checking based failure analysis approach,the requirement model of the on-board subsystem of CTCS-3train control system was first established using timed automata,while an event model depicting the failure scenario was constructed utilizing log data recorded during the failure.Next the combined model was model-checked in UPPAAL which then produced a counter-example path that described the system behavior in the failure event.By analyzing this path,errors in the requirement were found and eliminated,and the system was modified accordingly.An actual failure event in which a train with CTCS-3system accidentally initiated an emergency brake was analyzed using this approach and a requirement flaw was located.The modification towards this flaw was verified to be effective.

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

分 类 号：TP393[自动化与计算机技术—计算机应用技术] U283[自动化与计算机技术—计算机科学与技术]