剖析自动驾驶系统集成中的验证难题，探索形式化方法的应用路径。
Open Challenges in the Formal Verification of Autonomous Driving
- 以真实自动驾驶系统为案例，分析异构软硬件集成的验证难点。
- 针对黑箱组件无法披露内部行为的问题，提出形式化验证的应对思路。
- 适合关注自动驾驶安全与系统可靠性研究的工程师与学者。
在自动驾驶领域，高度复杂且异构系统的开发与集成已成为常态。现代车辆并非单一整体系统，而是由多种硬件组件构成，各自运行独立的软件系统。自动驾驶汽车包含多个由不同甚至可能竞争的公司开发的独立组件。这种多样性给认证过程带来巨大挑战，因为需要对可能不公开内部行为的组件（即黑箱）进行认证。本文通过一个真实的自动驾驶系统案例，识别其开发与集成中的关键开放性挑战，并探讨形式化验证技术如何解决这些问题，以确保系统的可靠性和安全性。
原文摘要 · Abstract (English)
In the realm of autonomous driving, the development and integration of highly complex and heterogeneous systems are standard practice. Modern vehicles are not monolithic systems; instead, they are composed of diverse hardware components, each running its own software systems. An autonomous vehicle comprises numerous independent components, often developed by different and potentially competing companies. This diversity poses significant challenges for the certification process, as it necessitates certifying components that may not disclose their internal behaviour (black-boxes). In this paper, we present a real-world case study of an autonomous driving system, identify key open challenges associated with its development and integration, and explore how formal verification techniques can address these challenges to ensure system reliability and safety.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。