One Stack, Diverse Vehicles: Checking Safe Portability of Automated Driving Software

TL;DR

The paper tackles the challenge of safely porting automated driving software across heterogeneous vehicle hardware, especially under OTA updates. It introduces a formal portability-checking framework that builds per-vehicle configuration models capturing dynamics, sensors, and actuators, derives a configuration-specific safe set $S_n$ within the operating domain $O_n$, and uses bounded model checking to verify that the closed-loop ACC remains in $S_n for all feasible parameters $p_n$ and disturbances $w$. The approach is demonstrated on two ACC implementations (a traditional MPC and a neural-network controller) across three vehicle configurations, providing rapid feedback on necessary adaptations and enabling rapid, safe integration of software or parameter updates. Key contributions include extending the modeling to cover sensor and actuator effects, incorporating actuation delays via Krasovskii augmentation, and applying a three-step verification for DNN-based controllers. Overall, the work shows that automatic, formal portability checks can streamline safe deployment for AD software across a diverse fleet and can be integrated into continuous integration processes, albeit with limitations related to model fidelity and low-level software.

Abstract

Integrating an automated driving software stack into vehicles with variable configuration is challenging, especially due to different hardware characteristics. Further, to provide software updates to a vehicle fleet in the field, the functional safety of every affected configuration has to be ensured. These additional demands for dependability and the increasing hardware diversity in automated driving make rigorous automatic analysis essential. This paper addresses this challenge by using formal portability checking of adaptive cruise controller code for different vehicle configurations. Given a formal specification of the safe behavior, models of target configurations are derived, which capture relevant effects of sensors, actuators and computing platforms. A corresponding safe set is obtained and used to check if the desired behavior is achievable on all targets. In a case study, portability checking of a traditional and a neural network controller are performed automatically within minutes for each vehicle hardware configuration. The check provides feedback for necessary adaptations of the controllers, thus, allowing rapid integration and testing of software or parameter changes.

Figures (3)

• Figure 1: A common automated driving architecture for vehicles 1 and 2. Differing components are colored in red and blue, respectively. Low-level controllers are configuration-specific, while each vehicle has an instance of the same high-level controller implementation.
• Figure 2: Portability checking for each vhc $n$: based on the odd $O_n$ and the model $\sigma_n$, the safe set $S_n$ is computed. Then, $S_n$ is used with the parameter set $P_n$ to check the safe closed-loop operation of the ACC software.
• Figure 3: Slices of the robust controlled invariant sets: 3D for $w_t=0$ and zero delayed inputs (upper plot), and 2D for additionally $v_{T}=20\,m/s$ (lower plot).