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

在智能轨道交通中,信号系统作为指挥列车安全运行的核心控制系统,在列车运行过程中,控制不当可能导致对人类生命,财产或环境造成灾难性后果。传统的自然语言描述使系统开发缺乏统一的标准,而形式化方法可以有效验证和评估系统设计正确性。文章研究了形式化安全保障技术在智能轨道交通领域的应用,针对全自动驾驶FAO系统中各子系统之间复杂的交互作用,文章结合了形式化方法和STPA方法。以车载ATP系统为例,进行形式化和安全分析方法的结合分析,按照STPA步骤进行安全分析,识别系统相关的安全约束,并运用了XSTAMPP软件辅助分析过程。研究结果实现了自然语言的安全需求到线性时序逻辑(LTL)的形式化规范的转化,有效避免了可能存在的二义性,体现了STPA与形式化结合方面的实际应用价值,并为接下来进行形式化验证提供参考。