📝 SummarXiv

Abstract

This technical report presents the detailed implementation of a Collision Avoidance System (CAS) for Unmanned Aerial Vehicles (UAVs), developed as a case study to demonstrate a rigorous methodology for achieving DO-178C compliance in safety-critical software. The CAS is based on functional requirements inspired by NASA's Access 5 project and is designed to autonomously detect, evaluate, and avoid potential collision threats in real-time, supporting the safe integration of UAVs into civil airspace. The implementation environment combines formal methods, model-based development, and automated verification tools, including Alloy, SPIN, Simulink Embedded Coder, and the LDRA tool suite. The report documents each phase of the software lifecycle: requirements specification and validation, architectural and detailed design, coding, verification, and traceability, with a strong focus on compliance with DO-178C Design Assurance Level B objectives. Results demonstrate that formal modelling and automated toolchains enabled early detection and correction of specification defects, robust traceability, and strong evidence of verification and validation across all development stages. Static and dynamic analyses confirmed code quality and coverage, while formal verification methods provided mathematical assurance of correctness for critical components. Although the integration phase was not fully implemented, the approach proved effective in addressing certification challenges for UAV safety-critical systems. \keywords Collision Avoidance System (CAS), Unmanned Aerial Vehicles (UAVs), DO-178C compliance, Safety-critical software, Formal methods, Model-based development, Alloy, SPIN model checker, Simulink Embedded Coder, LDRA tool suite, Software verification and validation, Traceability, Certification.