Remote UAV: A capability-based architecture with deterministic, evidence-grounded independent verification for PX4 SITL/Gazebo mission simulation

Abstract oftware-in-the-loop (SITL) simulation is widely used to validate unmanned aerial vehicle (UAV) control soft-ware before flight on real hardware, but a control module reporting “completed” is not, by itself, quantitative evidence that a flight objective was met. We present Remote UAV, a simulation framework built on PX4 SITL, Gazebo, and MAVSDK that enforces a strict separation between capability execution, evidence collection, and deterministic, independent verification. The system exposes four reusable capabilities – TAKEOFF-001, NAV-001, RETURN-HOME-001, and LAND-001 – composed into two interaction modes, continuous Single Flight and multi-waypoint Mission Builder, and verified by a Python verifier that recomputes pass/fail from frozen telemetry rather than trusting module self-reports. We formalize this architecture – capabilities as precondition–execution–postcondition tuples, verification as a pure function over frozen telemetry traces, mission-level correctness as a conjunction of child verdicts with explicit continuity, evidence-integrity, and terminal-state predicates, a four-class taxonomy partitioning module/verifier outcome pairs, and a Bernoulli retry model of simulator flight-readiness – and validate it on two separate evidence layers. On a development-time functional baseline (V7.0 Deployment Edi-tion/Package 1.0.0), a 190-case regression suite passes 190/190, a 50-flight NAV-001 soak test passes 50/50, and an illustrative eight-step mission passes with maximum inter-step continuity 0.973 m and terminal-home distance 0.771 m. On a separately frozen evaluation baseline (v1.6.1), isolated from development to prevent post-hoc patching, the full regression suite passes 3028/3028 in 152.19 s; a comparative campaign crosses capability self-report against the independent verifier over 30 requested mission cycles, of which 25 reach PX4/Gazebo flight-readiness and execute, yielding 100/100 AGREE-PASS capability outcomes (Wilson 95% CI 86.7–100% per capability) with zero SILENT-FAIL or V-ONLY-LENIENT classifications; a reliability/fault-injection smoke test confirms expected verdicts on normal flights and correctly rejects two injected-fault conditions (4/4); and a longitudinal resource smoke test over 26 consecutive flights shows file-descriptor count constant at 6, zero residual MAVSDK processes, and a position-error distribution of mean 0.094 m (SD 0.036 m, p95 = 0.133 m). Separately, flight-readiness itself is 25/30 (83.3%) within three initialization attempts but only 13/30 (43.3%) on the first attempt, and a simple independentretry Bernoulli model calibrated on the first-attempt rate predicts a three-attempt readiness probability of 81.8%, close to the 83.3% observed – evidence that PX4/Gazebo cold-start readiness, not capability logic, is this system’s dominant source of end-to-end variability. We report what remains open just as explicitly: the reliability and longitudinal studies above are smoke-scale qualifications of the measurement protocol, not the n ≥ 30-per-condition and ≥ 4 h campaigns the protocol itself specifies as the confirmatory target. These results indicate that the proposed architecture is a viable foundation for simulation-first regression, soak, and comparative evaluation, and for staged extension toward a real-UAV adapter and a supervised AI planning layer that cannot bypass the independent verifier.