AdaCore has posted a new version of its booklet AdaCore Technologies for Airborne Software: Supporting certification and tool qualification for DO-178C/ED-12C. This edition reflects the updates and enhancements to AdaCore’s toolsuites since the publication of the original booklet. It summarizes the DO-178C/ED-12C documentation suite (the core standard, its supplements, and the accompanying tool qualification guidance), explains AdaCore’s tools and technologies (the Ada and SPARK languages, the GNAT Pro development environments, and the static and dynamic analysis suites), and correlates these tools and technologies with specific objectives in DO-178C/ED-12C and its associated standards.

A unique aspect of the booklet is the use-case orientation of its analysis in one of the chapters, which focuses on three scenarios:

• Coding with Ada 2012

• Coding with Ada using Object Oriented Technology features

• Using SPARK and formal methods

The booklet shows how AdaCore’s tools and technologies support the various software development and verification activities associated with these scenarios and thereby help meet DO-178C/ED-12C objectives.

Please have a look, and learn from expert authors Quentin Ochem and Frédéric Pothon how you can leverage the Ada and SPARK languages, together with AdaCore’s tools and technologies, to reduce the time and effort in producing DO-178C/ED-12C certified software.

If you are not already familiar with DO-178C/ED-12C or Ada (and even if you are), read on; the remainder of this blog provides some background and context for these topics.

The role of DO-178C/ED-12C

When it comes to applications that need to be reliable and safe, airborne systems on commercial aircraft are at or close to the top of the list. Fortunately, and despite some close calls over the years, the software in our planes has been remarkably robust. When an airplane incident occurs – which is rare – and software is found to be a contributing factor, analysis almost always shows that the software had, in fact, correctly implemented its specified requirements. The problem is typically a defect in some other life cycle process (e.g., incorrect assumptions or an incomplete hazard analysis) and not a coding error or verification lapse.

The successful track record for airborne software is no accident (pardon the pun); it results from a safety culture and careful management at all stages of the software life cycle. And the foundation is a standard from RTCA in the US and EUROCAE in Europe: DO-178C/ED-12C, officially titled Software Considerations in Airborne Systems and Equipment Certification. This document, published in 2011, offers guidance covering the various software life-cycle processes. The guidance is captured in a set of objectives and their associated activities, which in turn specify requisite inputs and outputs. The emphasis is on verification, which, in DO-178C/ED-12C terms, means manual source code review, requirements-based testing, and/or automated analysis.

Supplements to DO-178C/ED-12C adapt and extend the guidance for use with Model-Based Development and Verification (DO-331/ED-18C), Object-Oriented Technology and Related Techniques (DO-332/ED-217), and Formal Methods (DO-333.ED-216). These supplements support the use of modern technologies for airborne software and constitute the main difference from DO-178B/ED-12B, the earlier version of the standard.

If a project uses an automated tool to reduce or eliminate a manual process, then the tool's output can be trusted (i.e., it does not need to be checked) provided that the tool has been qualified for use on that project. Qualification guidance appears in an associated standard, DO-330/ED-15 (Software Tool Qualification Considerations). DO-330/ED-15 is not specific to airborne software or DO-178C/ED-12C and can be used in other application domains.

DO-178C/ED-12C aims to provide confidence that the software performs its intended function and does not adversely affect safety. It is designed to prevent errors from being introduced but recognizes that, even with modern verification technologies, the complete absence of bugs cannot be guaranteed. The standard therefore attempts to mitigate the effect of any software failure. Since airborne systems contain components with different effects on aircraft safety, the guidance in DO-178C/ED-12C is calibrated to the component's software level, which reflects how a software failure can compromise airworthiness. The level ranges from E (a failure has no effect on aircraft safety) to A (a failure could lead to loss of aircraft). The guidance at higher software levels includes additional objectives that must be met (for example, Modified Condition/Decision Coverage at level A) and more rigorous practices (for example, independence of the coding and verification personnel at levels A and B). Analogously for the tool qualification effort: the Tool Qualification Level (TQL) for an automated tool ranges from TQL-5 (the tool cannot insert an error in the executable object code, but it may fail to detect an error) to TQL-1 (the tool can insert an error in software at Level A).

Annex A in DO-178C/ED-12C contains tables summarizing the guidance for the various life cycle processes, based on the software level. Likewise for Annex A in DO-330/ED-15, with guidance based on the tool's TQL.

To be honest... DO-178C is not a formal requirement for aircraft certification in the US. In fact, its guidance has very little to do with airborne software: the various activities spelled out in the standard constitute sound software engineering practice in general for high-assurance systems. The role of DO-178C, and its relationship to specific airworthiness requirements, are stated in the Federal Aviation Agency (FAA) Advisory Circular (AC) 20-115D (“Airborne Software Assurance – Using RTCA/DO-178C”):

The FAA finds RTCA/DO-178C ... acceptable as a means, but not the only means, for showing compliance with applicable airworthiness regulations for the software aspects of airborne systems and equipment.

These “applicable airworthiness regulations” are found in Title 14 Code of Federal Regulations (14 CFR), which details the requirements for the various kinds of aircraft (e.g., fixed-wing, rotorcraft) in a hierarchical classification scheme: category, class, and possibly lower levels. Aircraft of a given design have a specific type, which corresponds to a “leaf” in the hierarchy. A manufacturer showing compliance with the requirements for an aircraft type receives a Type Certificate, allowing planes of that type to operate in FAA-controlled airspace.

As an example, 14 CFR Part 25 specifies requirements for the Transport category, which corresponds to large, complex airplanes for passengers or freight (such as the Boeing 737 or Airbus 320). These requirements relate to the aircraft as a whole and its various functions and conditions (flight maneuvering envelope, trim control, etc.), as well as human factors considerations. They do not specify whether it is hardware or software that is responsible for meeting the requirements. Here is an excerpt:

§ 25.321 General.
…
(d) The significant forces acting on the airplane must be placed in equilibrium in a rational or conservative manner. The linear inertia forces must be considered in equilibrium with the thrust and all aerodynamic loads, while the angular (pitching) inertia forces must be considered in equilibrium with thrust and all aerodynamic moments, including moments due to loads on components such as tail surfaces and nacelles. Critical thrust values in the range from zero to maximum continuous thrust must be considered.

So officially, DO-178C is an FAA-accepted means of compliance with the regulatory requirements in Title 14 Code of Federal Regulations (14 CFR) . Although in principle other means of compliance could be used, in practice this has not occurred. DO-178C is the de facto standard for demonstrating the airworthiness of airborne software.

An exactly analogous situation arises with ED-12C, the EUROCAE alias for DO-178C. EASA’s AMC 20-115D is equivalent to FAA’s AC 20-115D, specifying ED-12C as an accepted means of compliance with the Certification Specifications (CS) series of airworthiness specifications. The CS series is analogous to 14 CFR, but reflecting different administrative authorities and with some minor variances in wording.

(As an aside, it’s an interesting question how compliance with DO-178C/ED-12C – a standard that focuses on software functional correctness – relates to safety, which is typically measured in terms of tolerable rates of occurrence or mean time between failures. For a detailed analysis of this issue, please see John Rushby’s paper New Challenges in Certification for Aircraft Software. Although based on DO-178B, his analysis applies equally to DO-178C/ED-12C.

The role of Ada

When it comes to programming languages that are the best match for writing software that needs to be reliable and safe, Ada is at or close to the top of the list. The language was specifically designed to support sound software engineering methods for large-scale embedded real-time systems. It was revolutionary in integrating breakthroughs in software development methodologies from the late 1960s and early 1970s into a coherent design, incorporating programming language innovations from academia and research labs. Think very strong typing, structured programming, data abstraction/information hiding, “programming in the large” / modularization, generic templates, exception handling, and high-level concurrency support inspired by the message-passing model known as Communicating Sequential Processes. Fixed-point types, which are essential in applications where the target hardware lacks native floating-point support, are part of the data type facility. The Ada design is based on Pascal syntax, and a useful side effect is the inclusion of scalar ranges. If an angle is supposed to be within the range 0.0 through 360.0, Ada supplies the syntax for expressing this requirement. The emphasis is on early error detection: type mismatches are caught at compile time, and errors like out-of-range array indices and null pointer dereferences are detected at run time with a well-defined effect (raising an exception).

All of this was in the initial version of the language, which was designed by a team led by Jean Ichbiah at CII-Honeywell-Bull in France. Ada was approved as an ANSI standard in 1983 (hence this version is generally denoted as Ada 83) and became an international standard in 1987 under the auspices of the International Organization for Standardization (ISO). Production-quality implementations like DEC Ada in 1984 made Ada a reality, and the language saw usage not only for US defense applications (where it was required) but also commercially. For example, the Boeing 777 is an Ada airplane.

The Ada standard has undergone several revisions since then, in response to user experience and the evolving programming language and software methodology landscape. Ada 95, designed by a team led by Tucker Taft at Intermetrics in the US, brought a variety of enhancements:

• Full Object-Oriented Programming support without the need for garbage collection;

• A generalized program structuring model (child libraries);

• A high-level but efficient mechanism for state-based mutual exclusion (protected types/objects);

• Additional data type functionality (unsigned types, generalized pointers);

• Facilities for smooth interfacing with other languages;

• Extensions to the predefined environment;

• Specialized Needs annexes for support of Systems Programming, Real-Time Systems, Numerics, Information Systems, and Safety / Security; and

• Other improvements for easier expressibility or higher efficiency.

A programming language is only as good as its implementations. Fortunately and importantly, a quality compiler targeted to academia with FLOSS licensing (Freely Licensed Open Source Software) was available for Ada 95 as soon as the standard was published. This was the first GNAT compiler, produced by a team at NYU that would go on to found AdaCore and commercialize the GNAT technology: Robert Dewar, Ed Schonberg, and Richard Kenner in New York; and Cyrille Comar and Franco Gasperoni in Paris. (As a historical note, the somewhat whimsical name “GNAT” was originally an acronym standing for “GNU NYU Ada Translator”. Actually, “GNAC” would have been more accurate, since the implementation was a bona fide compiler to assembly language based on the GNU gcc technology, and not a translator. The expansion has long since been abandoned, but the acronym has persisted.)

Subsequent revisions to the Ada standard were less extensive but brought important functionality. Ada 2005 fleshed out the language’s OOP support (adding Java-style interfaces and generalizing inter-module dependencies) while Ada 2012 brought comprehensive support for contract-based programming inspired by SPARK (subprogram pre- and postconditions, type/subtype invariants). This latter facility, in effect, allows expressing functional requirements as assertions in the source code, where they can be verified either statically or through run-time checks while also making the program intent clear to the human reader. The most recent version of the language standard, Ada 2022, added lightweight parallelism features and more generally enhanced the language’s expressiveness

Admittedly, there have been some skeptics. In his Turing Award lecture in 1980, Prof. Anthony Hoare criticized Ada as overly complex and argued that some of its features were dangerous (viz., exception handling). He felt that it was possible “to select a very powerful subset that would be reliable and efficient in implementation and safe and economic in use.” However, the language sponsors at the time (the US Department of Defense) had been burned in the past by subsetted language implementations, since source code portability was sacrificed, and a “no subsets” policy was enforced. If a vendor wanted to claim that their compiler implemented Ada, they needed to implement the full language and pass an extensive validation suite.

In retrospect, Prof. Hoare’s pessimism has not been borne out. The language complexity argument is not often raised today, for Ada or other languages, and the “no subsets” policy has a pragmatic escape. Although an Ada compiler has to implement the full language, the programmer can indicate via pragma Restrictions that specific features will not be used. This allows the implementation to provide a smaller, simpler, and more efficient run-time library – suitable, e.g., for software that needs to be certified under DO-178C/ED-12C – and the program will be rejected if it uses a restricted feature. In fact, this mechanism was used to define an efficient and deterministic subset of concurrency features – the so-called Ravenscar Profile, which has been part of the Ada standard since Ada 2005. The Ravenscar Profile advanced the state of the art in language design, providing concurrency support that is powerful enough to express typical idioms but simple and efficient enough to be used in certified safety-critical real-time software.

Interestingly, although “dangerous” is perhaps too strong a word, Prof. Hoare’s critique of exception handling was prescient. Exceptions complicate program analysis: when program control transfers to a handler, it is not necessarily clear where the exception was raised and what the program state was at the time. Exceptions interact with other language features and introduce semantic and run-time library complexity. As a result, exception functionality in some programming languages is restricted. For example, SPARK limits exception support in order to facilitate formal verification, while Rust encourages abnormal returns to be implemented through data values (e.g., Result or Option) rather than control flow (“panic”, in Rust terms). For Ada, pragma Restrictions can be used to limit exception handling, while a reasonable stylistic convention is to provide a single “last chance” handler at the top level of the program (for example, to deal with a hardware failure / reduced configuration or to generate diagnostic information for later offline analysis).

In short, Ada has stood the test of time and has more than fulfilled its intended purpose: a modern, common language for high-assurance real-time embedded systems. And as a formally verifiable subset of Ada, the SPARK language goes even further, facilitating mathematics-based proofs of program properties including correct information flows, absence of run-time errors, and even full functional correctness with respect to formally expressed requirements.

Section 4.4 of DO-178C/ED-12C states:

The basic principle [of error prevention] is to choose requirements development and design methods, tools, and programming languages that limit the opportunity for introducing errors, and verification methods that ensure that errors introduced are detected.

Ada, SPARK, and AdaCore’s software development environments satisfy this criterion. To learn more, check out AdaCore Technologies for Airborne Software: Supporting certification and tool qualification for DO-178C/ED-12C.