自动驾驶形式化验证中的开放挑战

文章预览

24年11月来自意大利Modena大学的论文“Open Challenges in the Formal Verification of Autonomous Driving”。 在自动驾驶领域，开发和集成高度复杂和异构的系统是标准做法。现代车辆不是单片系统；而是由不同的硬件组件组成，每个组件都运行自己的软件系统。自动驾驶汽车由许多独立的组件组成，这些组件通常由不同的、可能相互竞争的公司开发。这种多样性给认证过程带来了重大挑战，因为它需要认证可能不会泄露其内部行为（黑匣子）的组件。本文介绍一个自动驾驶系统的真实案例研究，确定了与其开发和集成相关的关键开放挑战，并探讨了形式化验证技术如何应对这些挑战以确保系统的可靠性和安全性。 如 [27] 所述，美国汽车工程师协会 (SAE) 将自动驾驶的设计目标定义为六个不同等级，从 0 级 (L-0) 到 5 级 (L-5)。这些等级代表了自动化的一个范围：L-0 表 ………………………………