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

与传统列控系统相比，全自动无人驾驶运营场景更加复杂多变，潜在的危险及致因具有更强的隐蔽性和复杂性，给运营安全带来了新的挑战。针对以上问题，提出一种STAMP(Systems-Theoretic Accident Model and Process)与模型检验相结合的复杂运营场景安全验证方法。首先，基于STAMP理论构建运营场景分层控制结构模型，辨识潜在的不安全控制行为、分析危险致因和安全约束；其次，定义分层控制结构模型与安全状态机模型间的基本转换规则，基于分层控制结构模型、安全约束和转换规则，构建运营场景安全状态机模型；最后，针对提取的安全约束，利用数据流图建立安全属性验证模型，结合模型检验技术，对运营场景安全状态机模型进行形式化验证。以全自动无人驾驶运营场景中列车自动进站停车为例，对方法进行验证分析。结果表明，当STAMP理论提取的安全约束通过了场景安全状态机模型的验证时，表示在该场景中对应的不安全控制行为没有发生且不导致相应危险。该方法结合系统安全分析与形式化建模验证的优势，降低了运营场景建模的难度，构建的运营场景形式化模型满足系统安全约束，可以作为全自动无人驾驶系统安全设计和安全...