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.

Translating natural language (NL) requirements into formal specifications such as Computation Tree Logic (CTL) is essential for improving the efficiency and scalability of formal verification, especially in safety-critical systems. This study evaluates the ability of Large Language Models (LLMs) to automate this process. We compare three approaches: fine-tuning the Mistral model, using GPT-4 in a few-shot learning setup, and a hybrid that feeds a BERT pattern classifier’s prediction to GPT-4. Using the Natural2CTL dataset, we assess strict logical accuracy and an ambiguity-tolerant accuracy, complemented by auxiliary semantic and structural operator similarity measures. Fine-tuning yields the strongest strict correctness and operator-structure fidelity, while the hybrid narrows the gap to fine-tuning and substantially improves over few-shot prompting alone. Residual errors across methods concentrate in path-quantifier selection, temporal granularity, and scoping in multi-clause requirements. Overall, LLMs can draft CTL candidates that are usable after lightweight normalisation, but they should be integrated into human-in-the-loop workflows with basic automated checks before use in high-assurance settings. • Benchmarks three LLM-based methods for NL-to-CTL translation. • Fine-tuned Mistral achieves 47.6% strict logical accuracy and 71.4% ambiguity-tolerant accuracy for CTL specification generation. • GPT-4 few-shot learning offers rapid prototyping but lower syntactic precision. • BERT-GPT hybrid balances pattern recognition and generative translation. • LLM automation reduces expert effort, but expert review remains critical for safety.

In the domain of formal verification, translating natural language (NL) requirements into Computation Tree Logic (CTL) specifications presents a notable challenge due to the disparity between human-readable documents and formal specifications. This paper introduces a novel approach that leverages Large Language Models (LLMs) to automate this translation process, thereby enhancing the accuracy and efficiency of formal verification practices. We fine-tune three state-of-the-art LLMs—LLAMA3, Mistral, and Qwen2—with a particular focus on optimizing the Mistral model due to its superior performance. Our methodology is supported by the Natural2CTL dataset, consisting of 2,095 NL requirements and their corresponding CTL specifications. We employ evaluation metrics such as validation loss, accuracy, semantic similarity, and Structural Operator Jaccard Similarity (SOJS) for a comprehensive assessment of model performance. Additionally, a comparative analysis with human translators, trained in CTL logic, underscores the LLMs’ potential to match or even surpass human accuracy in translating NL requirements into formal specifications. Our findings reveal that the fine-tuned Mistral model significantly outperforms the other LLMs and human participants, demonstrating superior accuracy in generating CTL specifications. This study advances the field of formal verification by proposing a scalable solution to the NL-to-CTL translation challenge, setting a new benchmark for the integration of AI tools in complex specification tasks.

Software development in critical airspace cyber-physical systems is challenging, mainly because of its safety-critical nature. Safety standards and regulations, such as DO-178C, provide guidelines for the development of software to ensure they adhere to the essential safety requirements in the certification processes. The requirements process proposed in the standard, which is responsible for developing the high-level requirements, is one of the most crucial steps in the life cycle since it serves as the basis for the subsequent processes. Having safety as a major concern, specifying safety requirements is of fundamental importance, allowing engineers to evaluate them and propose measures to mitigate the impact of a system failure, which can be catastrophic. In this paper, we present ReDaML, a domain-specific modelling language designed to support the development of safety-critical software systems, focused on the specification of high-level requirements in accordance with the DO-178C guidelines. Finally, a scenario of applying the approach to an UAS collision avoidance system is demonstrated.