Functional Requirements-Based Automated Testing for Avionics

TL;DR

This paper presents a formal, automated testing method using Bounded Model Checking to reduce manual effort in safety-critical avionics software testing, ensuring compliance with DO-178 standards.

Contribution

It introduces a novel formal approach for automatic test generation from low-level requirements, replacing labor-intensive manual testing processes in avionics software development.

Findings

Significantly reduces testing effort in avionics software qualification.

Maintains compliance with DO-178 safety standards.

Demonstrated effectiveness through industrial case studies.

Abstract

We propose and demonstrate a method for the reduction of testing effort in safety-critical software development using DO-178 guidance. We achieve this through the application of Bounded Model Checking (BMC) to formal low-level requirements, in order to generate tests automatically that are good enough to replace existing labor-intensive test writing procedures while maintaining independence from implementation artefacts. Given that existing manual processes are often empirical and subjective, we begin by formally defining a metric, which extends recognized best practice from code coverage analysis strategies to generate tests that adequately cover the requirements. We then formulate the automated test generation procedure and apply its prototype in case studies with industrial partners. In review, the method developed here is demonstrated to significantly reduce the human effort for the qualification of software products under DO-178 guidance.