Open Challenges in the Formal Verification of Autonomous Driving

In the realm of autonomous driving, the development and integration of highly complex and hetero-geneous systems are standard practice. Modern vehicles are not monolithic systems; instead, they arecomposed of diverse hardware components, each running its own software systems. An autonomousvehicle comprises numerous independent components, often developed by different and potentiallycompeting companies. This diversity poses significant challenges for the certification process, as itnecessitates certifying components that may not disclose their internal behaviour (black-boxes). Inthis paper, we present a real-world case study of an autonomous driving system, identify key openchallenges associated with its development and integration, and explore how formal verification tech-niques can address these challenges to ensure system reliability and safety.