Formal Safety and Robustness Verification of Nonlinear Vehicle Systems Under Uncertainty Using Sum-of-Squares Optimization

Ensuring stability and robustness in highly automated vehicle (HAV) control systems is critical for guaranteeing the safety of the intended functionality (SotiF) under real-world uncertainties inside a defined operational design domain (ODD). This paper presents a formal verification framework utilizing sum-of-squares (SOS) optimization to quantify and guarantee nonlinear system stability and robust performance in the presence of parametric uncertainties and environmental disturbances. We analyze a benchmark automated lane-following use case (UC) and verify polynomial system representations of the vehicle architecture against worst-case deviations using region of attraction (RoA) and robust positive invariant (RPI) sets. Simulation-based statistical validation using high-fidelity vehicle models confirms the effectiveness of the proposed method for formal robust control certification.