Verification and Validation of a Vision-Based Landing System for Autonomous VTOL Air Taxis

TL;DR

This work develops a Verification and Validation framework for vision-based landing of hybrid VTOL UAVs by integrating Verse-based reachability analysis with a high-fidelity CARLA-based simulation environment. It formalizes safety via $Reach(X_0, t)$ sets and validates performance through scenario-driven testing, including perception, path planning, and control components. The case study on the MiniHawk-VTOL demonstrates safe landings under varying initial conditions, landing-point uncertainties, and intruder presence, while examining the sim-to-real gap and the role of perception in refining landing targets. The approach provides mathematical safety guarantees and practical validation steps, offering a path toward robust deployment in cluttered urban environments, though it acknowledges the need for hardware-in-the-loop and outdoor experiments to further close the sim-to-real gap.

Abstract

Autonomous air taxis are poised to revolutionize urban mass transportation, however, ensuring their safety and reliability remains an open challenge. Validating autonomy solutions on air taxis in the real world presents complexities, risks, and costs that further convolute this challenge. Verification and Validation (V&V) frameworks play a crucial role in the design and development of highly reliable systems by formally verifying safety properties and validating algorithm behavior across diverse operational scenarios. Advancements in high-fidelity simulators have significantly enhanced their capability to emulate real-world conditions, encouraging their use for validating autonomous air taxi solutions, especially during early development stages. This evolution underscores the growing importance of simulation environments, not only as complementary tools to real-world testing but as essential platforms for evaluating algorithms in a controlled, reproducible, and scalable manner. This work presents a V&V framework for a vision-based landing system for air taxis with vertical take-off and landing (VTOL) capabilities. Specifically, we use Verse, a tool for formal verification, to model and verify the safety of the system by obtaining and analyzing the reachable sets. To conduct this analysis, we utilize a photorealistic simulation environment. The simulation environment, built on Unreal Engine, provides realistic terrain, weather, and sensor characteristics to emulate real-world conditions with high fidelity. To validate the safety analysis results, we conduct extensive scenario-based testing to assess the reachability set and robustness of the landing algorithm in various conditions. This approach showcases the representativeness of high-fidelity simulators, offering an effective means to analyze and refine algorithms before real-world deployment.

Figures (8)

• Figure 1: An overview of a simulation environment within CARLA with integrated air taxi.
• Figure 2: An overview of the simulation loop for the automated landing system in air taxis.
• Figure 3: Verification Architecture for VTOL landing system.
• Figure 4: A framework using simulated and real-world validation results to improve verified autonomy algorithms.
• Figure 5: Examples of helipad detection under different lighting conditions, photos are taken in CARLA from a downward-facing RGB camera attached to the belly of the aircraft.