DO-178C/ED-12C Guidance from AdaCore, as handbook download

Market news |
By Graham Prophet

This free booklet, “AdaCore Technologies for DO-178C / ED-12C”, written by Quentin Ochem (AdaCore) and certification expert Frédéric Pothon, addresses the DO-178C / ED-12C standards suite – the “core” DO-178C / ED-12C standard and its technology supplements – and explains many of their more subtle aspects in the context of several different development scenarios. In so doing, the booklet provides insights into how the Ada and SPARK languages, combined with AdaCore’s products and services, can help engineers develop and verify airborne software. Many of AdaCore’s tools have been qualified on safety-critical projects and have qualification material available; using a qualified tool can save considerable effort in demonstrating that various objectives in the DO-178C / ED-12C standards suite have been met.


“DO-178C is one of the most complex software safety standards in the industry,” said Quentin Ochem, lead of Business Development at AdaCore. “This booklet is aimed at software engineers and architects, to help them read between the lines of the standard and better understand the intent, using AdaCore’s technologies to illustrate how to meet the various requirements.”


The booklet approaches its subject matter from several angles. One chapter summarises the Ada and SPARK languages and describes various AdaCore tools, many of which have been qualified or are qualifiable for safety-critical systems:


– The GNAT Pro Assurance development environment, including support for “sustained branches”, which allows customers to evolve their software on a stable but maintained version of the GNAT Pro environment;

– The CodePeer advanced static analysis tool for Ada, which can find subtle bugs and vulnerabilities both during development and retrospectively on existing codebases;

– Basic static analysis tools, including the GNATcheck code standard enforcer and the GNATstack tool for computing maximum stack usage;

– Dynamic analysis tools: GNATtest (a test harness generator), GNATemulator (a target emulator), and GNATcoverage (a code coverage analyser at both the object and source levels, handling statement coverage, decision coverage, and modified condition/decision coverage);

– Integrated Development Environments: GNAT Programming Studio (GPS), GNATbench, and GNATdashboard; and

– The QGen model-based development and verification toolset, which includes a tuneable and qualifiable code generator from a safe subset of Simulink and Stateflow models to SPARK or MISRA-C.


One chapter shows how to exploit AdaCore’s technologies to comply with the guidance in the DO-178C / ED-12C suite, in the context of several development scenarios (use cases):


– Coding with Ada 2012 without using Object-Oriented Technology (OOT). This use case shows how AdaCore’s products and services contribute to the activities in the core DO-178C / ED-12C standard.

– Coding with Ada 2012 and using OOT. This use case takes into account the guidance in DO-332 / ED-217 (Object-Oriented Technologies and Related Techniques), in particular the objective of Local Type Consistency.

– Developing a design model and using a qualified code generator (QGen). This use case takes into account the guidance in DO-331 / ED-218 (Model-Based Development and Verification).

– Using SPARK and formal analysis. This use case takes into account DO-333 / ED-216 (Formal Methods) and explains how to gain credit for formal proofs to reduce or eliminate testing activities.


The DO-178C booklet is available as a pdf download from;


For a printed copy contact




Linked Articles
eeNews Embedded