Compositional code-level safety verification for automated driving controllers

Ensuring the safety of automated driving vehicles is particularly challenging due to the wide range of their operating conditions. This paper introduces CoCoSaFe, a Co mpositional Co de-level formal Sa fety verification F ram e work for automated driving controllers. Unlike traditional verification methods, such as model-based analysis, counterexample detection by guided simulation, or runtime verification through online monitoring, our approach verifies controller implementations directly at code level in an offline setting. Compositional contracts and bounded model checking are employed to assess the implementation of subsystem controllers against invariant sets. For neural network-based controllers, we introduce a scalable three-step decomposition method that utilizes a neural network verifier. CoCoSaFe is applied to adaptive cruise and lane-keeping controllers, for which we derive formal specifications and analytical models of the desired longitudinal and lateral behaviors, amenable for decoupled invariant sets. Various types of traditional and neural network controllers are verified in the order of minutes, showcasing its broad applicability and effectiveness in ensuring behavioral safety of software for automated driving and similar cyber–physical systems. • A framework for automated verification of automated driving controller safety at code-level. • Use of compositional contracts and bounded model checking for subsystem verification. • A scalable method for verifying neural-network-based controllers. • Effective application to traditional and neural-network adaptive cruise and lane keeping controllers.