论文标题
自动驾驶的正式验证的故障操作安全概念
A Formally Verified Fail-Operational Safety Concept for Automated Driving
论文作者
论文摘要
现代自动驾驶(AD)系统依靠安全措施来处理故障并将车辆带到安全状态。为了消除致命的道路事故,汽车制造商不断引入新的感知和控制系统。当代汽车设计和安全工程最佳实践适合隔离分析系统组件,而当今高度复杂且相互依存的AD系统需要新颖的方法来确保对多点故障的韧性。我们提出了一个整体安全概念,统一了处理多点故障的先进安全措施。我们提出的方法使设计师能够专注于更紧迫的问题,例如处理与系统性能限制相关的无故障危险行为。为了验证我们的方法,我们在正式规范语言MCRL2中开发了安全概念的可执行模型。模型行为受四模式退化策略控制分布式处理器,冗余通信网络和虚拟机的控制。为了使车辆尽可能安全,我们的退化政策可以使用其他低成本驾驶渠道来降低驾驶舒适度或广告系统的可用性。我们在模态mu-calculus中正式化了五个安全要求,并与我们的MCRL2模型证明了它们,这是使用传统的道路测试或模拟技术详尽完成的。总之,我们正式证明的安全概念定义了设计广告系统的整体设计模式。
Modern Automated Driving (AD) systems rely on safety measures to handle faults and to bring vehicle to a safe state. To eradicate lethal road accidents, car manufacturers are constantly introducing new perception as well as control systems. Contemporary automotive design and safety engineering best practices are suitable for analyzing system components in isolation, whereas today's highly complex and interdependent AD systems require novel approach to ensure resilience to multi-point failures. We present a holistic safety concept unifying advanced safety measures for handling multiple-point faults. Our proposed approach enables designers to focus on more pressing issues such as handling fault-free hazardous behavior associated with system performance limitations. To verify our approach, we developed an executable model of the safety concept in the formal specification language mCRL2. The model behavior is governed by a four-mode degradation policy controlling distributed processors, redundant communication networks, and virtual machines. To keep the vehicle as safe as possible our degradation policy can reduce driving comfort or AD system's availability using additional low-cost driving channels. We formalized five safety requirements in the modal mu-calculus and proved them against our mCRL2 model, which is intractable to accomplish exhaustively using traditional road tests or simulation techniques. In conclusion, our formally proven safety concept defines a holistic design pattern for designing AD systems.