The DO-178C standard (also known as ED-12C in Europe) for airborne software was released with an associated Formal Methods Suplement, DO-333 (also known as ED-216). This supplement describes how formal methods may be used to satisfy many of the requirements of DO-178C. Some DO-178C requirements, such as compliance of software requirements with system requirements, can be demonstrated by formal specifications and formal models of the software and the system of which it is part. Other requirements, such as compliance of source code with low-level requirements, are best met using formal tools that process source code annotated with low-level requirements.

How we can help

Perfect Developer supports software specification, architecture and refinement - with formal proof at all levels. Use it to specify, develop and model the the High Level Requirements, Software Architecture and Low Level Requirements of DO-178C, thereby providing traceability and formal proof of consistency between them. In many cases, Perfect Developer can also be used to develop a formal model of the system, and the System Requirements expressed. By this means, the software High Level Requirements can be verified against the System Requirements.

When using object-oriented design, Perfect Developer provides verification (by formal proof) of local type consistency in accordance with the Liskov Substitution Principle, as required by DO-332 - the Object Oriented Technology supplement to DO-178C.

Escher C Verifier (eCv) supports the development of code in MISRA-C (and some C++, if desired) using the Verified Design-by-Contract paradigm. The contracts - which express the low-level requirements - are mathematically proven to be honoured by both caller and callee - giving formal proof of correctness of the code with respect to the low level requirements. Naturally, eCv also proves that the software is free from undefined behaviour, and enforces use of a safe subset of C.

Escher Verification Studio delivers both Perfect Developer and Escher C Verifier in a single product, providing the means to generate formal proof of correctness at all levels, making it ideal for developing safety-critical airborne software. Alternatively, where Ada is the implementation language of choice, Perfect Developer can be paired with the SPARK Ada tools.

Both Perfect Developer and Escher C Verifier produce detailed proof traces and a verification summary report, for use as evidence when seeking certification. By generating proofs automatically, Perfect Developer and Escher C Verifier make the production of formally-verified software quick and economical.

Interested? Contact us for further details!