1. Introduction

This document explains how to use AdaCore's technologies — the company's tools, run-time libraries, and associated services — in conjunction with the safety-related standards for airborne software: DO ‑ 178C/ED ‑ 12C and and its technology supplements and tool qualification considerations. It describes how AdaCore's technologies fit into a project's software life cycle processes, and how they can satisfy various objectives of the standards. Many of the advantages of AdaCore's products stem from the software engineering support found in the Ada programming language, including features (such as contract-based programming) introduced in Ada 2012 [ISOIEC12]. Other advantages draw directly from the formally analyzable SPARK subset of Ada [AA20], [Dro22], [CDMM24]. As a result, this document identifies how Ada and SPARK contribute toward the development of reliable software. AdaCore personnel have played key roles in the design and implementation of both of these languages.

Although DO ‑ 178C/ED ‑ 12C doesn't prescribe any specific software life cycle, the development and verification processes that it encompasses can be represented as a variation of the traditional "V-model". As shown in Fig. 1, AdaCore's products and the Ada and SPARK languages contribute principally to the bottom portions of the V — coding and integration and their verification. The Table annotations in Fig. 1 refer to the tables in DO ‑ 178C/ED ‑ 12C and, when applicable, specific objectives in those tables.

../../../_images/introduction-fig1.png

Fig. 1 AdaCore Technologies and DO ‑ 178C/ED ‑ 12C Life Cycle Processes

Complementing AdaCore's support for Ada and SPARK, the company offers tools and technologies for C, C++ and Rust. Although C lacks the built-in checks as well as other functionality that Ada provides, AdaCore's Ada and C toolchains have similar capabilities. And mixed-language applications can take advantage of Ada's interface checking that is performed during inter-module communication.

AdaCore's Ada and C compilers can help developers produce reliable software, targeting embedded platforms with RTOSes as well as bare metal configurations. These are available with long term support, certifiable run-time libraries, and source-to-object traceability analyses as required for DO ‑ 178C/ED ‑ 12C Level A. Supplementing the compilers are a comprehensive set of static and dynamic analysis tools, including a code standard enforcer, a vulnerability and logic error detector, test and coverage analyzers, and a fuzzing tool.

A number of these tools are qualifiable with respect to the DO ‑ 330/ED ‑ 215 standard (Tool Qualification Considerations). The use of qualified tools can save considerable effort during development and/or verification since the output of the tools does not need to be manually checked. Qualification material, at the applicable Tool Qualification Level (TQL), is available for specific AdaCore tools.

Supplementing the core DO ‑ 178C/ED ‑ 12C standard are three supplements that address specific technologies:

  • DO-331/ED-218: Model-Based Development and Verification

    AdaCore's tools and technologies can be used in conjunction with model-based methods but do not relate directly to the issues addressed in DO ‑ 331/ED ‑ 218.

  • DO-332/ED-217: Object-Oriented Technology and Related Techniques

    The Ada and SPARK languages provide specific features that help meet the objectives of DO ‑ 332/ED ‑ 217, thus allowing developers to exploit Object Orientation (e.g., class hierarchies and inheritance for specifying data relationships) in a certified application.

  • DO-333/ED-216: Formal Methods

    The SPARK language and toolset directly support DO ‑ 333/ED ‑ 216, allowing the use of formal proofs to replace some low-level testing.

The technologies and associated options presented in this document are known to be acceptable, and certification authorities have already accepted most of them on actual projects. However, acceptance is project dependent. An activity using a technique or method may be considered as appropriate to satisfy one or several DO ‑ 178C/ED ‑ 12C objectives for one project (determined by the development standards, the input complexity, the target computer and system environment) but not necessarily on another project. The effort and amount of justification to gain approval may also differ from one auditor to another, depending of their background. Whenever a new tool, method, or technique is introduced, it's important to open a discussion with AdaCore and the designated authority to confirm its acceptability. The level of detail in the process description provided in the project plans and standard is a key factor in gaining acceptance.