一种用于自动驾驶的形式化验证失效可运行安全概念

现代自动驾驶（AD）系统依赖安全措施来处理故障并将车辆带入安全状态。为消除致命的道路交通事故，汽车制造商不断引入新的感知与控制系统。当代汽车设计和安全工程最佳实践适用于孤立地分析系统组件，而当今高度复杂且相互依赖的自动驾驶系统需要新颖的方法来确保对多点故障的弹性。我们提出了一种统一先进安全措施以处理多点故障的整体安全概念。我们提出的方法使设计人员能够专注于更紧迫的问题，例如处理与系统性能限制相关的无故障危险行为。为验证我们的方法，我们在形式化规范语言 mCRL2 中开发了该安全概念的可执行模型。模型行为由四模式降级策略控制，该策略管理分布式处理器、冗余通信网络和虚拟机。为尽可能保持车辆安全，我们的降级策略可利用额外的低成本驾驶通道降低驾驶舒适性或自动驾驶系统的可用性。我们在模态 μ-演算中形式化了五项安全要求，并针对我们的 mCRL2 模型进行了证明，而使用传统道路测试或仿真技术难以穷尽地完成此类证明。总之，我们形式化证明的安全概念为设计自动驾驶系统定义了一种整体设计模式。