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

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

1 概述

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

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

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