Hybrid verification improves safety checks of Autoware control node
Verifying Autoware Controller Node by Combining Model Verification and Runtime Monitoring
Software Engineering
Summary
It’s hard to be sure self-driving cars always behave safely because their control systems are complex. This work combines two ways to check safety: a mathematical proof of a simplified model and real-time checks while running the software. The authors formalized the Autoware control logic in a proof system to guarantee safety and progress. They then verified that the actual software stays close to the model during operation. Their tests showed the car's position and speed stayed accurate within small bounds.
What this means in practice
- •For autonomous vehicle engineers: Ensure trajectory-following controllers meet safety and accuracy expectations during development and testing.
- •For robotics system integrators: Monitor deployed autonomous robot controllers to verify they remain within verified safety bounds during operation.
Authors
Daisuke Ishii
Abstract
Formal modeling and verification of autonomous driving systems remain challenging due to the vast operational space and the complexity of the control logic. We propose a hybrid verification approach that combines formal model verification and runtime monitoring for the trajectory-following control node of Autoware, an open-source autonomous driving platform. We formalize the controller as a hybrid system in differential dynamic logic (dL), and introduce an abstract model that captures the essential control dynamics. We then prove safety and liveness properties of the model using the KeYmaera X proof assistant. Complementarily, we monitor the constraints that assure the compatibility between the model and the Autoware implementation across numerical simulation runs using the Autoware toolchain, quantifying to what extent the implementation's behavior is subsumed by the verified model. The experimental results confirmed that (i) monitoring provides a sound evaluation of target following with accuracy bounds, and (ii) the Autoware implementation reaches the target with an accuracy of approximately 0.2-0.4 (m) in position and 0.8 (m/s) in velocity.