arXiv preprint ·
Verifying Autoware Controller Node by Combining Model Verification and Runtime Monitoring
- Published
- Source
- arXiv preprint, posted before peer review
- Original
- Read it at arXiv
- Topics
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.
The authors’ abstract, as arXiv lists it. arXiv’s listings, abstracts included, are free for anyone to reuse.
Read it on ReadSearch
Each opens after you create an account, and brings you back to this paper.
More in Software Engineering
When Agent Evaluation Becomes Unreliable: An Empirical Study of Oracle Failures and Configuration-Dependent Measurement in an LLM Agent Benchmark
PassSum: Leveraging Paths of Abstract Syntax Trees and Self-Supervision for Code Summarization
SafeDSE: Joint Exploration of Safety Architecture Patterns, Mapping, and Scheduling for Dataflow Applications With Safety Arguments (Extended Version)
Comparing the Pre-trained Models of Source Code by Re-pre-training under a Unified Setup
EvoWeb: A Benchmark for Coding Agents on Evolving Web Applications
Get the few papers worth your time in Software Engineering every morning.
ReadSearch reads the new papers in your field each day and brings you the few worth reading, each with its key finding in a sentence.