在中国的铁路领域,列车运行控制系统是中国铁路的关键装备,是核心技术之一。列车运行控制系统是一种典型的安全苛求系统,一旦列车运行控制系统发生了失效行为,会造成十分严重的后果,轻则中断行车,重则导致重大财产损失甚至人员伤亡。因此,对列控系统的运营场景进行安全分析非常重要。本文研究了基于模型的安全分析方法,并给出了以接口自动机模型来描述系统行为的方法,根据接口自动机的语法语义刻画了系统组件与组件之间的交互行为,描述方式简洁,使用灵活,重用性高,提高了列控系统运营场景安全分析的质量和效率。本文主要研究工作如下:(1)采用接口自动机语言,对列控系统运营场景进行初步建模。根据接口自动机的语法语义定义了相关基本故障和传播故障,根据接口模型状态及动作迁移刻画了系统的故障行为。(2)基于接口自动机模型的安全分析需要各接口自动机组合后的状态空间作为计算目标。因为复杂系统状态空间十分庞大,给出了状态空间重构策略,将状态空间划分为安全区域、触发区域和危险区域,通过可达性分析,将移除无关动作迁移和合并同类状态,有效减少状态数量,实现状态空间重构。(3)改进了广度优先搜索算法,设计了启发式搜索算法,利用较小有界k值对搜索树做修剪,也就是用一个简单的可达路径作为指导来搜索状态空间内的所有路径,实现故障最小割集的生成。(4)为了实现接口自动机建模和安全分析的自动化,开发了一个面向接口自动机模型工具,该工具是利用Java Swing构建的图形化界面,集成了接口自动机建模,安全分析,故障树生成三大功能,可以较好地辅助本论文的研究工作。(5)结合CTCS-3级列控系统中RBC切换场景,严格对照RBC切换流程的规范,分析出其各个组件的状态、迁移路径、输入输出动作,考虑实际运营场景可能出现的故障事件,确定RBC切换系统的接口自动机模型。借助接口自动机模型工具,实现了模型的建立,应用算法对其安全分析后生成故障事件最小割集,并用故障树的形式展现分析结果。