The development of software for Unmanned Aerial Vehicles (UAVs) is governed by stringent safety-critical regulations, with DO-178C serving as the primary standard for airborne systems. Ensuring compliance requires extensive verification, validation, and traceability across the software lifecycle, which becomes increasingly complex for autonomous and adaptive UAV functions. This paper proposes an integrated methodology for regulatory compliance checking that combines formal methods with automated verification tools to generate certification-ready evidence under DO-178C. Formal methods are applied at multiple levels: Alloy is used for requirements consistency checking, the SPIN model checker for architectural interaction properties, and bounded model checking for code-level analysis. These techniques are integrated with automated toolchains that provide continuous bidirectional traceability, structural coverage analysis, and automated test execution across the software lifecycle. The approach is evaluated on a Design Assurance Level (DAL) B UAV Collision Avoidance System. The case study demonstrates the production of certification-ready evidence bundles, including closed bidirectional traceability from system requirements through high and low-level software requirements to source code and tests, formal proof summaries linked to requirements, and decision coverage reports on mission-critical logic. Results indicate that tightly integrating formal analysis with automated verification improves early defect detection, reduces manual evidence assembly, and strengthens the auditability of DO-178C compliance. The combined use of formal methods and automation offers a scalable pathway for UAVs and other autonomous systems to achieve compliance with evolving safety regulations. The findings highlight that integrating regulatory compliance checking into development processes can simultaneously enhance rigour and efficiency, providing a model for certifiable autonomy software in civil airspace. • Engineered a workflow that combines formal methods with automation for DO-178C UAV compliance. • End-to-end methodology validated on a UAV Collision Avoidance System case study. • Produced certification-ready evidence: traceability, proofs, and coverage. • Improved early defect detection and reduced manual certification effort. • Illustrates a scalable path for certifiable autonomy in safety-critical UAVs.
Zrelli et al. (Thu,) studied this question.