VeriODD: From YAML to SMT-LIB -- Automating Verification of Operational Design Domains
Bassel Rafie, Christian Schindler, Andreas Rausch
TL;DR
VeriODD automates the translation of YAML-based operational domain specifications into formal SMT-LIB language, enabling automated verification of autonomous driving safety boundaries.
Contribution
It introduces a tool that automates YAML to SMT-LIB translation, integrating formal verification into stakeholder-friendly specifications for autonomous driving.
Findings
Automates translation from YAML to SMT-LIB for verification.
Enables automated consistency checks of ODD specifications.
Provides a user-friendly GUI for editing and verification.
Abstract
Operational Design Domains (ODDs) define the conditions under which an Automated Driving System (ADS) is allowed to operate, while Current Operational Domains (CODs) capture the actual runtime situation. Ensuring that a COD instance lies within the ODD is a crucial step in safety assurance. Today, ODD and COD specifications are frequently expressed in YAML to remain accessible for stakeholders, but such descriptions are not directly suitable for solver-based verification. Manual translation into formal languages such as SMT-LIB is slow and error-prone. We present VeriODD, a tool that automates this translation. VeriODD uses ANTLR-based compiler technology to transform YAML-based ODD/COD specifications into both human-readable propositional logic, for lightweight review on a simple basis, and solver-ready SMT-LIB. The tool integrates with SMT solvers such as Z3 to provide automated…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSafety Systems Engineering in Autonomy · Formal Methods in Verification · Autonomous Vehicle Technology and Safety