基于STAMP与模型检验的全自动无人驾驶复杂运营场景安全验证方法  

Safety Verification of Fully Automatic Driverless System Complex Operation Scenario Based on STAMP and Model Checking

作　　者：马牧云 张亚东[1,2] 李耀 郭进 MA Muyun;ZHANG Yadong;LI Yao;GUO Jin(School of Information Science and Technology,Southwest Jiaotong University,Chengdu 611756,China;Sichuan Train Control Technology Engineering Research Center,Chengdu 611756,China;School of Software Engineering,Chengdu University of Information Technology,Chengdu 610225,China)

机构地区：[1]西南交通大学信息科学与技术学院,成都611756 [2]四川省列车运行控制技术工程研究中心,成都611756 [3]成都信息工程大学软件工程学院,成都610225

出　　处：《铁道标准设计》2024年第3期198-207,共10页Railway Standard Design

基　　金：四川省科技计划项目(2021YJ0070);中央高校基本科研业务费专项资金资助项目(2682022ZTPY084)。

摘　　要：与传统列控系统相比,全自动无人驾驶运营场景更加复杂多变,潜在的危险及致因具有更强的隐蔽性和复杂性,给运营安全带来了新的挑战。针对以上问题,提出一种STAMP(Systems-Theoretic Accident Model and Process)与模型检验相结合的复杂运营场景安全验证方法。首先,基于STAMP理论构建运营场景分层控制结构模型,辨识潜在的不安全控制行为、分析危险致因和安全约束;其次,定义分层控制结构模型与安全状态机模型间的基本转换规则,基于分层控制结构模型、安全约束和转换规则,构建运营场景安全状态机模型;最后,针对提取的安全约束,利用数据流图建立安全属性验证模型,结合模型检验技术,对运营场景安全状态机模型进行形式化验证。以全自动无人驾驶运营场景中列车自动进站停车为例,对方法进行验证分析。结果表明,当STAMP理论提取的安全约束通过了场景安全状态机模型的验证时,表示在该场景中对应的不安全控制行为没有发生且不导致相应危险。该方法结合系统安全分析与形式化建模验证的优势,降低了运营场景建模的难度,构建的运营场景形式化模型满足系统安全约束,可以作为全自动无人驾驶系统安全设计和安全改进的重要基础。Compared with the traditional train control system,the fully automatic driverless operation scenario is more complex and changeable,and the potential hazards and their causes are more imperceptible,which brings new challenges to operation safety.To solve these problems,a safety verification method for complex operation scenarios is proposed,which combines STAMP with model checking.Firstly,a hierarchical control structure model of operation scenarios is constructed to identify potential unsafe control behaviors and analyze the risk causes,as well as safety constraints.Secondly,the basic transition rules between the hierarchical control structure model and the safe state machine model are defined,and the safe state machine model of the operation scenario is built based on the model and transition rules.Finally,for the security constraints,a safety attribute verification model is established by using the data flow graph.Combined with the formal verification technology,the safe state machine model of the operation scenario is verified.In this paper,the method is validated and analyzed with reference to the automatic train parking in the fully automatic driverless operation scenario.The result shows that when the safety constraints extracted from the STAMP theory pass the verification of the scenario security state machine model,it means that the corresponding unsafe control behavior in the scenario does not occur and does not lead to the corresponding danger.By combining the advantages of system safety analysis and formal modeling verification,this method reduces the difficulties of operation scenario modeling and constructs a formal model of operation scenario that meets the safety constraints,which can be used as a basis for the safety design and safety improvement of fully automatic driverless system.

关 键 词：轨道交通 STAMP 模型检验 全自动无人驾驶系统 运营场景 STPA 安全状态机 SCADE 

分 类 号：U283[交通运输工程—交通信息工程及控制] U284.48[交通运输工程—道路与铁道工程]