Certification-Oriented Requirements and Model Verification Methodology for UAV Systems

The paper presents a certification-oriented methodology for requirements management and model verification in the design of unmanned aerial vehicle (UAV) systems. The proposed approach addresses challenges in certifying safety-critical UAV platforms whose architectures include custom-developed hardware and software components. The methodology integrates requirements engineering, functional hazard analysis (FHA), and formal model verification into a unified design and validation workflow. Methods for categorizing, prioritizing, and decomposing system requirements are presented to support the development of reliable UAV software and operational procedures. A systematic approach for mapping certification requirements and FHA safety functions to UAV operational scenarios and system use cases is introduced, enabling traceability between safety requirements, system behavior, and verification artifacts. The proposed framework employs Unified Modeling Language (UML) state-machine models, validated using linear temporal logic (LTL) and computation tree logic (CTL). Model verification is performed using the NuSMV symbolic model checker to assess the correctness, completeness, consistency, and safety properties of operational scenarios. A practical case study concerning UAV handover between ground control stations (GCSs) demonstrates the applicability of the proposed method. The analysis identifies inconsistencies in the operational model and shows how formal verification supports the early detection of unsafe or incomplete system behaviors. The presented approach supports the development of certification-ready UAV systems by improving requirements traceability, reducing verification ambiguities, and facilitating the validation of safety-critical flight-control procedures.