形式化的安全分析方法在智能轨道交通的应用

刘莎晨，韩 涛，朱天民，李思远

（卡斯柯信号有限公司北京分公司，北京 100160）

1 概述

形式化方法基于数学基础，可运用计算机的工具进行检查和分析验证[1]。铁路行业的安全相关标准EN50129也推荐了形式化方法，“系统安全完整性等级SIL为SIL3或SIL4时，推荐采用形式化方法对系统设计和开发一致性进行校验”[2]。

全自动驾驶（Fully Automatic Operation，FAO）系统作为智能轨道交通的必然发展趋势，近年来得到了广泛关注。FAO通过自动控制系统代替列车驾驶员、调度员执行的工作，减少了人为失误对系统安全运行的影响。针对FAO系统这种功能复杂、组件交互频繁、交互信息量大、时序特征复杂的系统，对其采用形式化的安全分析方法也势在必行。卡斯柯作为轨道交通信号行业的先进技术企业，自主研发了国产化的TRANAVI列车运行控制系统。为保障系统的“自主可控，安全可信”，卡斯柯也致力于形式化方法的研究，包括形式化方法建模、验证以及测试等多方面的研究，并运用于在安全保障领域。

在轨道交通领域，国内外学者也对系统安全分析方法进行了研究，验证了STAMP及STPA用于铁路安全分析的可行性[3]。文献[4]从系统论的角度分析了甬温线高铁事故，不仅考虑了设备故障和人为失误，还考虑了整个社会技术系统。此外，应用STPA对CBTC系统进行了分析，以识别事故场景，但对控制器内部算法没有展开说明。John Thomas[5]提出了不安全的控制行为的生成算法，该算法基于过程模型中的系统变量，自动生成不适当的控制行为。文献[6]以CTCS-1级列控系统RDC为研究对象，结合了STPA的安全分析与UPPAAL的建模和校验，对安全分析的结果进行了验证。

目前安全分析和形式化方法的结合在智能轨道交通领域的应用较少，针对以上现实背景以及面临的挑战，结合形式化方法和安全分析的STAMP理论，本文以FAO车载ATP为研究对象，按照STPA的步骤进行安全分析。

2 STPA概述

2004年，麻省理工学院的Nancy Leveson首先提出了基于系统理论的STAMP[7]模型。STAMP将安全定义为一个控制问题，认为导致事故的原因是控制不足或与安全相关的约束执行不力，而非组件的故障或失效。基于STAMP模型，Leveson提出了用于危险致因分析的STPA方法。

STPA的分析步骤如图1所示。

图1 STPA的步骤

3 应用实例：基于STPA与形式化结合的车载ATP分析方法

3.1 步骤一：定义系统级危害及安全约束

车载设备ATP根据速度-距离模式曲线监控列车运行，为避免列车运行时与其他列车相撞，对应的安全需求为在列车运行时，车载设备要确保列车与前车保持安全距离。事故，危害及安全约束如表1所示。

3.2 步骤二：建立控制结构

本文选择车载ATP作为控制器，列车接口单元TIU作为执行器，车载ATP通过TIU输出接口向列车输出制动指令。车载ATP通过SDU获取列车速度信息，通过BTM接收应答器的信息，获取列车位置信息。通过TIU输入接口获取列车制动的反馈信息。

利用XSTAMPP工具，建立列车紧急制动和缓解的控制过程的控制结构模型，如图2所示。

3.3 步骤三：识别不安全的控制行为

根据STPA方法论中提供的四种引导词，结合控制结构的控制行为。利用XSTAMP进行UCA的识别。UCA如表2所示。

使用XSTAMPP工具，可以选择生成上下文表，从而得到车载设备的系统行为规则，如图3所示。

安全需求转换为中文描述如下：

SR1：当车载ATP处于SM模式（列车ATP防护下的驾驶模式）时，速度超过允许速度（紧急制动干预速度），速度误差小于规定值，ATP应施加紧急制动。

SR2：当车载ATP处于SM模式时，列车越过行车许可终点时，ATP应施加紧急制动。

SR3：当车载ATP处于SM模式时，速传输入的速度差值超过规定值，ATP应该施加紧急制动。

表1 事故、危害及安全约束

图2 车载ATP控制结构

表2 不安全的控制行为

图3 车载ATP行为规则

图4 致因场景

图5 LTL形式化规范

SR4：当车载处于RM模式（限制人工驾驶模式），速度超过允许速度（固定限制速度如20km/h），速度误差小于规定值，ATP应施加紧急制动。

SR5：车载ATP输出紧急制动后，当列车速度大于0，不能缓解紧急制动。

SR6：车载ATP输出紧急制动后，当列车速度未知时，不能缓解紧急制动。

3.4 步骤四：识别致因场景

根据系统的功能处理过程，以及STPA方法论中所定义的分析引导图。识别列车制动未实施的原因以及安全需求。

通过XSTAMPP工具自动将危险控制措施转换为线性时间逻辑LTL的形式化语句，可用于日后的验证活动。如图5所示。

例如：SSR1.30 的 LTL 表达式为（（（（（Mode==SM）&&（SDU SpeedGappermitspeed）））→（（controlAction==Emergencybrake））））该表达式意为：当列车处于SM模式时，速度超过允许速度（紧急制动干预速度），速度误差小于规定值，ATP应施加紧急制动。与需求SR1相一致。

4 结论与未来工作

本文将基于STPA的方法与形式化方法进行结合，利用形式化的分析工具来辅助STPA的分析过程。本文完成的工作如下：（1）从系统层面，找出了车载ATP对列车控制过程中的危险，同时确定了相应的安全约束。（2）建立了车载系统的控制结构，并根据四种引导词，分析得到其不安全控制行为。（3）建立了包含过程模型的车载ATP的控制结构。（4）致因场景分析，即通过遍历控制回路，找出可能导致不安全控制行为的原因。（5）通过XSTAMPP软件工具来辅助分析过程，使得分析更加准确和完整，最终细化的安全需求包含自然语言描述和LTL形式化语言的表述。

随着大数据、云计算、物联网等先进技术的发展，智能轨道交通，从传统的信号系统，逐渐走向轨道交通的互联化、网络化。比如随着5G（第5代移动通信）技术的发展，在下一代的基于车车通信的列控系统中，可以进一步缩短列车运行间隔，甚至实现列车的近距离的同步运行，即虚拟编组。由此可能给列车运行安全带来新的挑战。STPA是基于系统理论的安全分析方法，还有XSTAMPP等软件辅助分析过程，对于复杂系统的功能安全分析更具优势。而形式化方法采用严谨的手段，逻辑精确，无二义性。因此在接下来的工作中，进一步探索STPA的应用范围，研究STPA方法与形式化验证相结合的分析方法，能更好的保障智能轨道交通的安全，提升系统性能。