Publikation
Finding a Needle in a Haystack: Scenario Coverage Verification for Single-UAV Missions Using SMT
Qurrat Ul Ain; Abhoy Kole; Muhammad Hassan; Rolf Drechsler
In: IEEE International Conference on Omni-Layer Intelligent Systems (COINS). IEEE International Conference on Omni-layer Intelligent Systems (IEEE COINS-2026), September 7-9, Bologna, Italy, 2026.
Zusammenfassung
In this paper, we propose an SMT-based framework
for scenario coverage verification of single-UAV missions under
bounded environmental assumptions. We present an abstract
mission-level model of a single UAV in a bounded 3D environment. The model captures mission states, stepwise 3D motion,
battery depletion, obstacles, NFZ, and altitude constraints. Mission failure is represented by an emergency state corresponding
to loss of safe recoverability. The SMT query searches for an
admissible environment configuration and a corresponding execution that violates the mission requirements. A satisfiable result
yields a concrete counterexample scenario, while an unsatisfiable
result establishes bounded correctness over the modeled scenario
family. The key contribution is lifting bounded verification from
individual system instances to families of systems defined over
a symbolic environment parameter space, enabling quantified
reasoning over all admissible environment configurations within
a single SMT query. This enables exhaustive scenario coverage
within bounded assumptions, which is not provided by finite
sampling-based validation within the same bounded setting.
Keywords—Uncrewed aerial vehicles, formal verification, satisfiability modulo theories, scenario co