在自动驾驶领域，开发和集成高度复杂且异构的系统是标准做法。现代车辆并非单体系统；相反，它们由各种硬件组件构成，每个组件运行其自身的软件系统。自动驾驶车辆包含许多独立组件，通常由不同且可能相互竞争的公司开发。这种多样性给认证过程带来了重大挑战，因为它需要对可能不公开其内部行为（黑盒）的组件进行认证。本文以一个自动驾驶系统的真实案例研究为例，确定其开发和集成过程中面临的关键开放性挑战，并探讨形式化验证技术如何应对这些挑战，以确保系统的可靠性和安全性。