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

摘要：

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

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

所属期刊栏目：39

分类号：TP393;U283(计算技术、计算机技术)

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

在线出版日期：2017-05-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共12页

页码：59-70