中文摘要：

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.