AdaCore Technologies for

DO-178C / ED-12C
Version 1.1

Frédéric Pothon and Quentin Ochem
March 2017

About the Authors
Frédéric Pothon
Frédéric Pothon is an independent consulting engineer with more than 25
years of experience in the development and certification of criticalsoftware (DO-178/ED-12, Levels A, B, and C). He has led projects at
Turboméca and Airbus, where he was responsible for software
methodologies and quality engineering processes, and he founded thecompany ACG-Solutions in 2007. Mr. Pothon is an expert in thequalification and utilization of automatic code generation tools for modelbased development, and he served as co-chair of the Tool Qualification
subgroup during the DO-178C/ED-12C project. He was also a memberof the EUROCAE/RTCA group that produced DO-248B/ED-94B, which
provides supporting information for DO-178B/ED-12B. Mr. Pothon isbased in Montpellier, France.

Quentin Ochem
Quentin Ochem is the Lead of Business Development and TechnicalAccount Management at AdaCore, a role that entails expanding thecompany's product reach in domains such as avionics, railroad, space, anddefense systems. Mr. Ochem has a software engineering backgroundand more than ten years of experience in the Ada programming
language, with a special focus on development and verification tools forsafety- and mission-critical systems. He has conducted customer training
on the Ada language, AdaCore tools, and the DO-178B and DO-178C
software certification standards, and has published numerous articles fortechnical trade journals. Mr.Ochem is based in AdaCore's New York
office.

iii

iv

Foreword
The guidance in the DO-178C / ED-12C standard and its associatedtechnology-specific supplements helps achieve confidence that airborne
software meets its requirements. Certifying that a system complies withthis guidance is a challenging task, especially for the verification
activities, but appropriate usage of qualified tools and specialized runtime libraries can significantly simplify the effort. This document explains
how a number of technologies offered by AdaCore – tools, libraries, andsupplemental services – can help. It covers not only the “core” DO-178C /ED-12C standard but also the technology supplements: Model-Based
Development and Verification (DO-331 / ED-218), Object-Oriented
Technology and Related Techniques (DO-332 / ED-217), and Formal
Methods (DO-333 / ED-216). The content is based on the authors’ many
years of practical experience with the certification of airborne software,with the Ada and SPARK programming languages, and with thetechnologies addressed by the DO-178C / ED-12C supplements.
The authors gratefully acknowledge the assistance of Ben Brosgol(AdaCore) for his review of and contributions to the material presented inthis document.
Frédéric Pothon, ACG Solutions
Montpellier, France
March 2017

Quentin Ochem, AdaCore
New York, NY
March 2017v

vi

AdaCore Technologies for DO-178C / ED-12C
Contents
About the Authors .................................................................................................. iii
Foreword v
1.

Introduction........................................................................................ 112.

The DO-178C/ED-12C Standards Suite ...................................... 14

2.1.

Overview............................................................................................. 14

2.2.

Software Tool Qualification Considerations:DO-330/ED-215............................................................................... 16

2.3.

Object Oriented Technology and Related Techniques
Supplement: DO-332 / ED-217..................................................... 17

2.4.

Model-Based Development and Verification Supplement:
DO-331 / ED-218 ............................................................................ 18

2.5.

Formal Methods Supplement: DO-333 / ED-216 ..................... 19

3.

AdaCore Tools and Technologies Overview ........................... 22

3.1.

Ada ...................................................................................................... 22

3.1.1.

Language Overview ......................................................................... 23

3.2.

SPARK .................................................................................................. 27

3.2.1.

Flexibility............................................................................................. 28

3.2.2.

Powerful Static Verification............................................................. 28

3.2.3.

Ease of Adoption ............................................................................... 28

3.2.4.

Reduced Cost and Improved Efficiency of Executable Object
Code (EOC) verification ................................................................... 29

3.3.

GNAT Pro Assurance ........................................................................ 29

3.3.1.

Sustained Branches............................................................................ 30

3.3.2.

Configurable Run-Time Library ...................................................... 30

3.3.3.

Full Ada 83 to 2012 Implementation ............................................ 30

3.3.4.

Source to Object Traceability ......................................................... 30

vii

3.3.5.

Safety-Critical Support and Expertise .......................................... 31

3.4.

CodePeer ............................................................................................ 31

3.4.1.

Early Error Detection......................................................................... 31

3.4.2.

Qualified for usage in Safety-Critical Industries ........................ 32

3.5.

Basic Static Analysis tools ................................................................ 32

3.5.1.

ASIS, GNAT2XML .............................................................................. 32

3.5.2.

GNATmetric ........................................................................................ 33

3.5.3.

GNATcheck ......................................................................................... 33

3.5.4.

GNATstack .......................................................................................... 34

3.6.

Dynamic Analysis Tools .................................................................... 36

3.6.1.

GNATtest............................................................................................. 36

3.6.2.

GNATemulator ................................................................................... 37

3.6.3.

GNATcoverage.................................................................................. 37

3.7.

Integrated Development Environments (IDEs) ............................... 38

3.7.1.

GNAT Programming Studio (GPS) ................................................. 38

3.7.2.

Eclipse support - GNATbench ......................................................... 39

3.7.3.

GNATdashboard ............................................................................... 39

3.8.

Model-Based Development: QGen ............................................... 39

3.8.1.

Support for Simulink® and Stateflow® models ............................ 40

3.8.2.

Qualification material ...................................................................... 40

3.8.3.

Support for model static analysis .................................................. 41

3.8.4.

Support for Processor-in-the-Loop testing .................................... 41

4.

Compliance with DO-178C / ED-12C Guidance: Analysis .. 42

4.1.

Overview............................................................................................. 42

4.2.

Use case #1a: Coding with Ada 2012 ........................................ 45

4.2.1.

Benefits of the Ada language ........................................................ 45

4.2.2.

Using Ada during the design process ............................................ 52

4.2.2.1 Component identification ................................................................ 53
4.2.2.2. Low-Level Requirements ................................................................. 55
viii

4.2.2.3. Implementation of Hardware/Software Interfaces .................. 58
4.2.3.

Integration of C components with Ada.......................................... 62

4.2.4.

Robustness / defensive programming ........................................... 63

4.2.5.

Defining and Verifying a Code Standard with GNATcheck
and GNAT2XML ................................................................................ 67

4.2.6.

Checking source code accuracy and consistency with
CodePeer ............................................................................................ 69

4.2.7.

Checking worst case stack consumption with GNATstack .......... 70

4.2.8.

Compiling with the GNAT Pro compiler ........................................ 71

4.2.9.

Using GNATtest for low-level testing ............................................ 72

4.2.10.

Using GNATemulator for low-level and software / software
integration tests ................................................................................. 76

4.2.11.

Structural code coverage with GNATcoverage .......................... 78

4.2.12.

Data and control coupling coverage with GNATcoverage ...... 82

4.2.13.

Demonstrating traceability of source to object code ................. 84

4.3.

Use case #1b: Coding with Ada using OOT features ............... 86

4.3.1.

Object orientation for the architecture ......................................... 86

4.3.2.

Coverage in the case of generics .................................................. 87

4.3.3.

Dealing with dynamic dispatching and substitutability.............. 89

4.3.4.

Dispatching as a new module coupling mechanism .................... 98

4.3.5.

Memory management issues ........................................................... 99

4.3.6.

Exception handling .......................................................................... 102

4.3.7.

Overloading and type conversion vulnerabilities ..................... 105

4.3.8.

Accounting for dispatching in performing resource analysis .. 106

4.4.

Use case #2: Developing a design model and using aqualified code generator (QGen) ............................................... 108

4.4.1.

Model development / verification and code generation ....... 108

4.4.2.

Contributions to model verification .............................................. 110

4.4.3.

Qualification credit on source code verification objectives .... 111

ix

4.4.4.

Qualification credit on Executable Object Code verification
objectives .......................................................................................... 112

4.4.5.

Qualification credit on structural code coverage ..................... 115

4.5.

Use case #3: Using SPARK and formal analysis....................... 117

4.5.1.

Using SPARK for design data development .............................. 117

4.5.2.

Robustness and SPARK ................................................................... 119

4.5.3.

Contributions to Low Level Requirement reviews ...................... 120

4.5.4.

Contributions to architecture reviews........................................... 121

4.5.5.

Contributions to source code reviews .......................................... 122

4.5.6.

Formal analysis as an alternative to low level testing ............. 125

4.5.7.

Low level verification by mixing test and proof(“Hybrid verification”) .................................................................... 126

4.5.8.

Alternatives to code coverage when using proofs ................... 128

4.5.9.

Property preservation between source code andobject code ....................................................................................... 129

4.6.

Parameter Data Items .................................................................... 130

5.

Summary of contributions to DO-178C/ED-12C objectives133

5.1 Overall summary: which objectives are met ......................................... 133
5.2 Detailed summary: which activities are supported .............................. 135
Table A-1 Software Planning Process .................................................. 136
Table A-2 Software Development Processes...................................... 138
Table A-4 Verification of Outputs of Software Design Process ..... 139
Table A-5 Verification of Outputs of Software Coding &Integration Processes ........................................................... 139
Table A-6 Testing of Outputs of Integration Process ........................ 141
Table A-7 Verification of Verification Process Results ...................... 142
References ........................................................................................................... 144

xFrédéric Pothon & Quentin Ochem

1. Introduction
This document explains how to use AdaCore’s technologies – thecompany’s tools, run-time libraries, and associated services – inconjunction with the safety-related standards for airborne software: RTCA
DO-178C / EUROCAE ED-12C 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 underlying
Ada programming language, or from the SPARK Ada subset. As a result,
this document identifies how Ada and SPARK contribute toward thedevelopment of reliable software. AdaCore personnel have played key
roles in the design and implementation of both of these languages.
Although DO-178C doesn’t prescribe any specific software life cycle, thedevelopment and verification processes that it encompasses can be
represented as a variation of the traditional “V” cycle. As shown in Figure
1, AdaCore’s products and the Ada and SPARK languages contribute
principally to the bottom portions of the “V” – coding and integration andtheir verification. The Table annotations in Figure 1 refer to the tables in
DO-178C / ED-12C and, when applicable, specific objectives in thosetables.

11

AdaCore Technologies for DO-178C / ED-12C

HLR &Integration
TestingHigh-Level
Requirements
Table A-2: 1,2
Table A-3

Ada and SPARK
languages

Development
Processes

Verification
Processes

Table A-6: 1, 2, 5
Table A-7

GNATemulator,
GNATcoverage,
GNATtest

Low Level
Requirements
Testing

SoftwareDesignTable A-2: 3,4,5
QGen model
Table A-4
code generator

Table A-6: 3, 4
Table A-7

QGen model verifierand debugger

Ada and SPARK
languages

Software Coding
Table A-2: 6,7

Ada and SPARK languages,
GNAT Compiler,
GNAT IDEs (GPS, GNATbench)

Table A-5

CodePeer, SPARK tools,
GNATcheck, GNATstack, GNATmetric,
GNATdashboard

Figure 1: AdaCore Technologies andDO-178C / ED-12C Life Cycle Processes

AdaCore also offers tools and technologies for projects using the C
language. Although C lacks the built-in checks as well as otherfunctionality that Ada provides, AdaCore’s Ada and C toolchains have
similar capabilities. And mixed-language applications can takeadvantage of Ada’s interface checking that is performed during intermodule communication.
AdaCore’s Ada and C compilers can help developers produce reliable
software, targeting embedded platforms with RTOSes as well as “baremetal” 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 tools including coding standard checkers, test
and coverage analyzers, and static analysis tools.
A number of these tools are qualifiable with respect to the DO-330 / ED215 recommendations (Tool Qualification Considerations). The use ofqualified tools can save considerable effort during development and/or
verification since the output of the tools does not need to be manuallychecked. Qualification material, at the applicable Tool Qualification Level(TQL), are available for specific AdaCore tools.
Supplementing the core DO-178C/ED-12C standard are three
supplements that address specific technologies:
12

Frédéric Pothon & Quentin Ochem

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



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

DO-333/ED-216: Formal Methods

AdaCore’s tools make it easier to comply with these supplements:


QGen, a qualifiable code generator for model-based
development, accepts a safe subset of Simulink® and Stateflow®
models and generates SPARK and MISRA-C. Certification credit
for the use of a qualified code generator may be claimed onmost of the source code verification objectives and low-leveltesting.

Ada and SPARK provide specific features that help meet theobjectives of DO-332/ED-217, thus allowing developers tospecify a hierarchy of classes in a certified application.

The SPARK language and technology directly support DO333/ED-216, allowing the use of formal proofs in place of lowlevel testing.

The technologies and associated options presented in this document are
known to be acceptable, and certification authorities have alreadyaccepted 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 notnecessarily 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 isintroduced, it’s important to open a discussion with AdaCore and thedesignated authority to confirm its acceptability. The level of detail in theprocess description provided in the project plans and standard is a key
factor in gaining acceptance.

13

AdaCore Technologies for DO-178C / ED-12C

2. The DO-178C/ED-12C
Standards Suite
2.1. Overview“Every State has complete and exclusive sovereignty over the airspace
above its territory.” This general principle was codified in Article 1 of theConvention on International Civil Aviation (the “Chicago Convention”) in
1944. To control the airspace, harmonized regulations have beenformulated to ensure that the aircraft are airworthy.
A type certificate is issued by a certification authority to signify the
airworthiness of an aircraft manufacturing design. The certificate reflects
a determination made by the regulating body that the aircraft is
manufactured according to an approved design, and that the design
complies with airworthiness requirements. To meet those requirements theaircraft and each subassembly must also be approved. Typically,requirements established by a regulating body refer to “Minimum
Operating Performance Standards” (MOPS) and a set of recognized“Acceptable Means of Compliance” such as DO-178/ED-12 for software,
DO-160/ED-14 for environmental conditions and test procedures, andDO-254/ED-80 for Complex Electronic Hardware.
DO-178C/ED-12C – Software Considerations in Airborne Systems andEquipment Certification – was issued in December 2011, developed jointly
by RTCA, Inc., and EUROCAE. It is the primary document by which
certification authorities such as the FAA, EASA, and Transport Canada
approve all commercial software-based aerospace systems.
The DO-178C/ED-12C document suite includes:


14

The core document, which is a revision of the previous release(DO-178B/ED-12B). The changes are mostly clarifications, andalso address the use of “Parameter Data Items” (e.g.,
Configuration tables)Frédéric Pothon & Quentin Ochem

DO-278A/ED-109A, which is similar to DO-178C/ED-12C andaddresses ground-based software used in the domain of
CNS/ATM (Communication Navigation Surveillance/Air Traffic
Management)

DO-248C/ED-94C (Supporting Information for DO-178C/ED12C and DO-278A/ED-109A), which explains the rationale
behind the guidance provided in the core documents

Three technology-specific supplementsoooDO-331/ED-218: Model Based Development andVerification
DO-332/ED-217: Object Oriented Technology and
Related Techniques
DO-333/ED-216: Formal Methods

Each supplement adapts the core document guidance asappropriate for its respective technology. These supplements are
not standalone documents but must be used in conjunction with
DO-178C/ED-12C or DO-278A/ED-109A


The Tool Qualification Considerations document (DO-330/ED215), providing guidance for qualifying software tools

One of the main principles of these documents is to be “objectiveoriented”. The guidance in each document consists of a set of objectives
that relate to the various software life-cycle processes (planning,development, verification, configuration management, quality assurance,
certification liaison). The objectives that must be met for a particular
software component depend on the software level (also known as a Design
Assurance Level or DAL) of the component. The level in turn is based on thepotential effect of an anomaly in that software component on thecontinued safe operation of the aircraft. Software levels range from E(the lowest) where there is no effect, to A (the highest) where an anomaly
can cause the loss of the aircraft. A software component’s level isestablished as part of the system life-cycle processes.
To gain software approval for a system, the applicant has to demonstratethat the objectives relevant to the software level for each component

15

AdaCore Technologies for DO-178C / ED-12C

have been met. To achieve this goal, the development team specifies thevarious software life-cycle activities (based on those recommended by
DO-178C/ED-12C and/or others), and its associated methods,
environment, and organization/management. In case the chosen methods
are addressed by one of the technology supplements, additional or
alternative objectives must also be satisfied. The technology supplements
may replace or add objectives and/or activities.

2.2. Software Tool Qualification Considerations:DO-330/ED-215
A software tool needs to be qualified when a process is automated,
eliminated, or reduced, but its outputs are not verified. The systematic
verification of the tool outputs is replaced by activities performed on thetool itself: the “tool qualification”. The qualification effort depends on theassurance level of the airborne software and the possible effect that anerror in the tool may have on this software. The resulting combination, theTool Qualification Level, is a 5 level scale, from TQL-5 (the lowest level,
applicable to software tools that cannot insert an error in the resulting
software, but might fail to detect an error) to TQL-1 (the highest,
applicable to software tools that can insert an error in software atlevel A).
A tool is only qualified in the context of a specific project, for a specificcertification credit, expressed in term of objectives and activities.
Achieving qualification for a tool on a specific project does of course
greatly increase the likelihood of being able to qualify the tool onanother project. However, a different project may have different
processes or requirements, or develop software with different
environment constraints. As a result, the qualifiability of a tool needs to besystematically assessed on a case-by-case basis.
Although many references are made in the literature about “qualified”
tools, strictly speaking this term should only be used in the context of a
specific project. Tools provided by tool vendors, independently of any
project, should be identified as “qualifiable” only. The tool qualification
document guidance (DO-330/ED-215) includes specific objectives thatcan only be satisfied in the context of a given project environment.

16

Frédéric Pothon & Quentin Ochem

Throughout this document, the applicable tool qualification level is
identified together with the relevant objective or activity for which credit
may be sought. The qualification activities have been performed withrespect to DO-330/ED-215 at the applicable Tool Qualification Level.
Tool qualification material is available to customers as a supplement to
AdaCore’s GNAT Pro Assurance product.

2.3. Object Oriented Technology and Related
Techniques Supplement: DO-332 / ED-217
Although DO-332 / ED-217 is often referred as the “object oriented
supplement”, the “related techniques” mentioned in the title are equally
relevant and are addressed in detail. They may be used in conjunction
with Object-Oriented Technology (OOT) but are not necessarily related
to OO features. Such “related techniques” include virtualization,
genericity (also known as templates), exceptions, overloading, anddynamic memory management.
Considering the breadth of features covered by DO-332/ED-217, atleast some of its guidance should be followed regardless of whether theactual application is using object orientation. For example, typeconversion is probably present in most code bases regardless of which
language is being used.
The DO-332 / ED-217 supplement is much more code-centric than theothers, and only two objectives are added: one related to local typeconsistency (dynamic dispatching) and another one related to dynamic
memory. All other guidance takes the form of additional activities forexisting DO-178C / ED-12C objectives.
Of particular relevance is the supplement’s Vulnerability Analysis annex.
Although not binding, it explains in detail what is behind these additional
activities. The following features in particular may need to be addressed
when Ada is used:

Inheritance / local type consistencyParametric polymorphism (genericity)Overloading17

AdaCore Technologies for DO-178C / ED-12C

Type conversion



Exception managementDynamic memoryComponent-based development

The Ada language, the precautions taken during the design and coding
processes, and the use of AdaCore tools combine to help address or
mitigate the vulnerabilities associated with these features.

2.4. Model-Based Development and Verification
Supplement: DO-331 / ED-218
A model is defined as “an abstract representation of a given set of
aspects of a system that is used for analysis, verification, simulation, code
generation, or any combination thereof”. The supplement identifies two
kinds of models: specification models that express the High-Level
Requirements, and design models expressing the software architecture
and/or Low-Level Requirements.
Model-based development covers a wide range of techniques forrepresenting the software requirements and/or architecture, most often
through a graphical notation. The source code itself is not considered as amodel. Well known examples include UML for software architecture,
SysSML for system representation, and Simulink® for control algorithms
and related requirements. DO-331 / ED-218 presents the objectives andactivities associated with the use of such techniques. The main added
value of the supplement is its guidance on how to use model simulationand obtain certification credit.
Model-based development might not be appropriate for capturing thecomplete set of system aspects. For example, while a large part of theanalog control code can be effectively modeled by Simulink®, it would
typically be easier to use traditional requirements definition methods(most notably natural language) to express I/O, low level layers, orcomplex logic.

18

Frédéric Pothon & Quentin Ochem

In the context of AdaCore’s technology, the focus is on design models thatcan be used to express control algorithms or state machines, namely
Mathworks’ Simulink® and Stateflow® languages. These are typically used
to represent a subset of the software’s low-level requirements. The
correctness of these requirements can be verified in a simulation
environment. Model simulation is therefore an appropriate and efficienttechnique to verify that the requirements expressed in the model are acorrect and complete implementation of the higher level of requirements.
This higher level is referred to as “requirements from which the model isdeveloped”.
Design models are translated into source code, for example C or Ada,
either manually or automatically. The way to convert the model into
source code – i.e., manually or through a code generator (qualified ornot) – is not addressed in the supplement. Additional information isprovided in the Tool Qualification Considerations standard (DO-330/ED215) concerning the use of a qualified code generator or the verificationof the outputs of a non-qualified code generator.
The AdaCore technology relevant to this supplement is QGen, aqualifiable model-based toolsuite that includes a code generator (TQL-1)
for a safe subset of Simulink® and Stateflow® models, and a model
verification capability that can identify potential run-time errors and also
support proof of safety properties at the model level. The code
generator is tunable and can generate SPARK/Ada or MISRA-C. A model
debugger is also available for QGen, providing a synchronized view
across the model, the generated source code, and the compiled object
code.

2.5. Formal Methods Supplement: DO-333 /ED-216
DO-333 / ED-216 provides guidance on the use of formal methods. A
formal method is defined as “a formal model combined with a formal
analysis”. A formal model should be precise, unambiguous and have amathematically defined syntax and semantics. The formal analysis should
be sound; i.e., if it is supposed to determine whether the formal model (forexample the software source code in a language such as SPARK) satisfies

19

AdaCore Technologies for DO-178C / ED-12C

a given property, then the analysis should never assert that the property
holds when in fact it does not.
A formal method may be used to satisfy DO-178C/ED-12C verification
objectives; formal analysis may therefore replace some reviews, analyses
and tests. Almost all verification objectives are potential candidates forformal methods.
In DO-178C / ED-12C, the purpose of testing is to verify the Executable
Object Code (EOC) based on the requirements. The main innovation of
DO-333 / ED-216 is to allow the use of formal methods to replace somecategories of tests. In fact, with the exception of software / hardware
integration tests showing that the EOC is compatible with the target
computer, the other objectives of EOC verification may be satisfied byformal analysis. This is a significant added value. However, employing
formal analysis to replace tests is a new concept in the avionics domain,with somewhat limited experience in practice thus far (see [1] for further
information). Details from tool providers on the underlying models ormathematical theories implemented in the tool are necessary to assess thematurity of the method. Then substantiation and justification need to be
documented, typically in the PSAC, and provided to certification
authorities at an early stage for review.
AdaCore provides the SPARK technology as a formal method that caneliminate or reduce the testing based on low-level requirements. Using
SPARK will also get full or partial credit for other objectives, such as
requirements and code accuracy and consistency, verifiability, etc. Its
usage is consistent with the example provided in Appendix B of DO333/ED-216, “FM.B.1.5.1 Unit Proof”. Certification credit for using formal
proofs is summarized in Figure 2:

20

Frédéric Pothon & Quentin Ochem

System Requirements

High Level
Requirements

Low Level
Requirements

Software Architecture

impliedSoftware architecture iscompliantby Formal Proof

Source Code
Source Code isaccurate and consistent
by Formal Proof

Consistency
Verifiability

Executable Object
Code

Compliance
Robustness
by Formal Proof

Property
Preservation

Figure 2: SPARK contributions to verification objectives

21

AdaCore Technologies for DO-178C / ED-12C

3. AdaCore Tools andTechnologies Overview
3.1. Ada
Ada is a modern programming language designed for large, long-lived
applications – and embedded systems in particular – where reliability,
maintainability, and efficiency are essential. It was originally developedin the early 1980s (this version is generally known as Ada 83) by a teamled by Jean Ichbiah at CII-Honeywell-Bull in France. The language wasrevised and enhanced in an upward compatible fashion in the early
1990s, under the leadership of Tucker Taft from Intermetrics in the U.S.
The resulting language, Ada 95, was the first internationally standardized(ISO) object-oriented language. Under the auspices of ISO, a further(minor) revision was completed as an amendment to the standard; thisversion of the language is known as Ada 2005. Additional features(including support for contract-based programming in the form ofsubprogram pre- and postconditions and type invariants) were added in
the most recent version of the language standard, Ada 2012 (see [2] [3][4] for information about Ada).
The name “Ada” is not an acronym; it was chosen in honor of Augusta
Ada Lovelace (1815-1852), a mathematician who is sometimes regarded
as the world’s first programmer because of her work with Charles
Babbage. She was also the daughter of the poet Lord Byron.
Ada is seeing significant usage worldwide in high-integrity / safetycritical / high-security domains including commercial and military aircraft
avionics, air traffic control, railroad systems, and medical devices. With its
embodiment of modern software engineering principles Ada is an
excellent teaching language for both introductory and advanced
computer science courses, and it has been the subject of significant
university research especially in the area of real-time technologies.
AdaCore has a long history and close connection with the Ada
programming language. Company members worked on the original Ada
22

Frédéric Pothon & Quentin Ochem

83 design and review and played key roles in the Ada 95 project as wellas the subsequent revisions. The initial GNAT compiler was essential to thegrowth of Ada 95; it was delivered at the time of the language’s
standardization, thus guaranteeing that users would have a quality
implementation for transitioning to Ada 95 from Ada 83 or otherlanguages.

3.1.1.

Language Overview

Ada is multi-faceted. From one perspective it is a classical stack-based
general-purpose language, not tied to any specific development
methodology. It has a simple syntax, structured control statements,
flexible data composition facilities, strong type checking, traditionalfeatures for code modularization (“subprograms”), and a mechanism fordetecting and responding to exceptional run-time conditions (“exception
handling”).
But it also includes much more:
Scalar ranges
Unlike languages based on C syntax (such as C++, Java, and C#), Ada
allows the programmer to simply and explicitly specify the range ofvalues that are permitted for variables of scalar types (integer, floatingpoint, fixed-point, and enumeration types). The attempted assignment ofan out-of-range value causes a run-time error. The ability to specify
range constraints makes programmer intent explicit and makes it easier todetect a major source of coding and user input errors. It also provides
useful information to static analysis tools and facilitates automated proofs
of program properties.
Here’s an example of an integer scalar range:
Score : Integer range 1..100;
N: Integer;...
Score := N;-- A run-time check verifies that N is within the range 1..100-- If this check fails, the Constraint_Error exception israised23

AdaCore Technologies for DO-178C / ED-12C

Contract-based programming
Ada 2012 allows extending a subprogram specification or a
type/subtype declaration with a contract (a Boolean assertion).
Subprogram contracts take the form of preconditions and postconditions;type contracts are used for invariants, and subtype contracts provide
generalized constraints (predicates). Through contracts the developer canformalize the intended behavior of the application, and can verify thisbehavior by testing, static analysis or formal proof.
Here’s a skeletal example that illustrates contact-based programming; aTable object is a fixed-length container for distinct Float values.
package Table_Pkg istype Table is private;-- Encapsulated typeprocedure Insert (T : in out Table; Item: in Float)
with Pre => not Is_Full(T) and not Contains(T, Item),
Post => Contains(T, Item);procedure Remove (T : in out Table; Item: in Float);with Pre => Contains(T, Item),
Post => not Contains(T, Item);function Is_Full (T : in Table) return Boolean;function Contains (T : in Table; Item: in Float) return
Boolean;...
private...
end Table_Pkg;

A compiler option controls whether the pre- and post-conditions arechecked at run time. If checks are enabled, a failure raises theAssertion_Error exception.
Programming in the large
The original Ada 83 design introduced the package construct, a featurethat supports encapsulation (“information hiding”) and modularization,
and which allows the developer to control the namespace that isaccessible within a given compilation unit. Ada 95 introduced the concept
of “child units,” adding considerable flexibility and easing the design of24

Frédéric Pothon & Quentin Ochem

very large systems. Ada 2005 extended the language’s modularization
facilities by allowing mutual references between package specifications,thus making it easier to interface with languages such as Java.
Generic templates
A key to reusable components is a mechanism for parameterizing modules
with respect to data types and other program entities, for example astack package for an arbitrary element type. Ada meets this requirement
through a facility known as “generics”; since the parameterization is doneat compile time, run-time performance is not penalized.
Object-Oriented Programming (OOP)
Ada 83 was object-based, allowing the partitioning of a system intomodules corresponding to abstract data types or abstract objects. Full
OOP support was not provided since, first, it seemed not to be requiredin the real-time domain that was Ada’s primary target, and, second, theapparent need for automatic garbage collection in an OO language
would have interfered with predictable and efficient performance.
However, large real-time systems often have components such as GUIs
that do not have real-time constraints and that could be most effectively
developed using OOP features. In part for this reason, Ada 95 supplies
comprehensive support for OOP, through its “tagged type” facility:classes, polymorphism, inheritance, and dynamic binding. Ada 95 does
not require automatic garbage collection but rather supplies definitionalfeatures allowing the developer to supply type-specific storage
reclamation operations (“finalization”). Ada 2005 brought additional
OOP features including Java-like interfaces and traditional obj.op(...)
operation invocation notation.
Ada is methodologically neutral and does not impose a “distributed
overhead” for OOP. If an application does not need OOP, then the OOP
features do not have to be used, and there is no run-time penalty.
See [4] or [5] for more details.
Concurrent programming
Ada supplies a structured, high-level facility for concurrency. The unit ofconcurrency is a program entity known as a “task.” Tasks can communicate
implicitly via shared data or explicitly via a synchronous control

25

AdaCore Technologies for DO-178C / ED-12C

mechanism known as the rendezvous. A shared data item can be defined
abstractly as a “protected object” (a feature introduced in Ada 95), with
operations executed under mutual exclusion when invoked from multiple
tasks. Asynchronous task interactions are also supported, specificallytimeouts and task termination. Such asynchronous behavior is deferredduring certain operations, to prevent the possibility of leaving shareddata in an inconsistent state. Mechanisms designed to help takeadvantage of multi-core architectures were introduced in Ada 2012.
Systems programming
Both in the “core” language and the Systems Programming Annex, Ada
supplies the necessary features for hardware-specific processing. For
example, the programmer can specify the bit layout for fields in arecord, define alignment and size properties, place data at specificmachine addresses, and express specialized code sequences in assembly
language. Interrupt handlers can also be written in Ada, using theprotected type facility.
Real-time programming
Ada’s tasking facility and the Real-Time Systems Annex support common
idioms such as periodic or event-driven tasks, with features that can help
avoid unbounded priority inversions. A protected object locking policy isdefined that uses priority ceilings; this has an especially efficient
implementation in Ada (mutexes are not required) since protected
operations are not allowed to block. Ada 95 defined a task dispatchingpolicy that basically requires tasks to run until blocked or preempted, andAda 2005 introduced several others including Earliest Deadline First.
High-integrity systems
With its emphasis on sound software engineering principles Ada supports
the development of high-integrity applications, including those that need
to be certified against safety standards such DO-178B / ED-12B andDO-178C / ED-12C for avionics, CENELEC EN 50128 for rail systems
and security standards such as the Common Criteria. For example, strong
typing means that data intended for one purpose will not be accessed via
inappropriate operations; errors such as treating pointers as integers (orvice versa) are prevented. And Ada’s array bounds checking prevents
buffer overflow vulnerabilities that are common in C and C++.

26

Frédéric Pothon & Quentin Ochem

However, the full language may be inappropriate in a safety-criticalapplication, since the generality and flexibility could interfere withtraceability / certification requirements. Ada addresses this issue by
supplying a compiler directive, pragma Restrictions, that allows
constraining the language features to a well-defined subset (for example,
excluding dynamic OOP facilities).
The evolution of Ada has seen the continued increase in support forsafety-critical and high-security applications. Ada 2005 standardized theRavenscar Profile, a collection of concurrency features that are powerfulenough for real-time programming but simple enough to makecertification practical. Ada 2012 has introduced contract-based
programming facilities, allowing the programmer to specify preconditions
and/or postconditions for subprograms, and invariants for encapsulated(private) types. These can serve both for run-time checking and as input tostatic analysis tools.
In brief, Ada is an internationally standardized language combining
object-oriented programming features, well-engineered concurrency
facilities, real-time support, and built-in reliability through both compiletime and run-time checks. As such it is an appropriate language foraddressing the real issues facing software developers today. Ada is usedthroughout a number of major industries to design software that protects
businesses and lives.

3.2. SPARKSPARK is a software development technology (programming language
and verification toolset) specifically designed for engineering ultra-low
defect level applications, for example where safety and/or security are
key requirements. SPARK Pro is AdaCore’s commercial-grade offering of
the SPARK technology. The main component in the toolset is GNATprove,
which performs formal verification on SPARK code.
SPARK has an extensive industrial track record. Since its inception in thelate 1980s it has been used worldwide in a range of industrial
applications such as civil and military avionics, air traffic management /control, railway signaling, cryptographic software, and cross-domain
solutions. SPARK 2014 is the most recent version of the technology (see
[6]).
27

AdaCore Technologies for DO-178C / ED-12C

3.2.1.

Flexibility

SPARK 2014 offers the flexibility of configuring the language on a perproject basis. Restrictions can be fine-tuned based on the relevant coding
standards or run-time environments.
SPARK 2014 code can easily be combined with full Ada code or with C,
so that new systems can be built on and reuse legacy codebases.

3.2.2.

Powerful Static Verification

The SPARK 2014 language supports a wide range of static verification
techniques. At one end of the spectrum is basic data and control flow
analysis, i.e., exhaustive detection of errors such as attempted reads ofuninitialized variables, and ineffective assignments (where a variable isassigned a value that is never read). For more critical applications,dependency contracts can constrain the information flow allowed in an
application. Violations of these contracts – potentially representing
violations of safety or security policies – can then be detected even
before the code is compiled.
In addition, the language supports mathematical proof and can thus
provide high confidence that the software meets a range of assurance
requirements: from the absence of run-time exceptions, to the enforcementof safety or security properties, to compliance with a formal specificationof the program’s required behavior.

3.2.3.

Ease of Adoption

The SPARK 2014 technology is easy to learn and can be smoothly
integrated into an organization’s existing development and verification
methodology and infrastructure.
Pre-2014 versions of the SPARK language used a special annotation
syntax for the various forms of contracts. In SPARK 2014 this has been
merged with the standard Ada 2012 contract syntax, which both
simplifies the learning process and also allows new paradigms ofsoftware verification. Programmers familiar with writing executable
contracts for run-time assertion checking can use the same approach butwith additional flexibility: the contracts can be verified either dynamically28

Frédéric Pothon & Quentin Ochem

through classical run-time testing methods or statically (i.e., precompilation and pre-test) using automated tools.
SPARK supports “hybrid verification” that can mix testing with formal
proofs. For example an existing project in Ada and C can adopt SPARK
to implement new functionality for critical components. The SPARK units
can be analyzed statically to achieve the desired level of verification,with testing performed at the interfaces between the SPARK units and themodules in the other languages.

3.2.4.
Reduced Cost and Improved Efficiency
of Executable Object Code (EOC) verification
Software verification typically involves extensive testing, including unit
tests and integration tests. Traditional testing methodologies are a major
contributor to the high delivery costs for safety-critical software.
Furthermore, they may fail to detect errors. SPARK 2014 addresses thisissue by allowing automated proof to be used to demonstrate functionalcorrectness at the subprogram level, either in combination with or as areplacement for unit testing. In the high proportion of cases where proofs
can be discharged automatically the cost of writing unit tests is completely
avoided. Moreover, verification by proofs covers all execution conditions
and not just a sample.

3.3. GNAT Pro Assurance
GNAT Pro Assurance is an Ada and C development environment for
projects requiring specialized support, such as bug fixes and “known
problems” analyses, on a specific version of the toolchain. This productline is especially suitable for applications with long maintenance cycles orcertification requirements, since critical updates to the compiler or otherproduct components may become necessary years after the initial
release. Such customized maintenance of a specific version of the productis known as a “sustained branch”.

Based on the GNU GCC technology, GNAT Pro Assurance supports all
versions of the Ada language standard, from Ada 83 to Ada 2012, andalso handles multiple versions of C (C89, C99, and C11). It includes an
Integrated Development Environment (GNAT Programming Studio and/or

29

AdaCore Technologies for DO-178C / ED-12C

GNATbench), a comprehensive toolsuite including a visual debugger, anda set of libraries and bindings.

3.3.1.

Sustained Branches

Unique to GNAT Pro Assurance is a service known as a “sustainedbranch”: customized support and maintenance for a specific version of the
product. A project on a sustained branch can monitor relevant known
problems, analyze their impact, and if needed update to a newer versionof the product on the same development branch (i.e., not incorporatingchanges introduced in later versions of the product).
Sustained branches are a practical solution to the problem of ensuring
toolchain stability while allowing flexibility in case an upgrade is needed
to correct a critical problem.

3.3.2.

Configurable Run-Time Library

GNAT Pro Assurance includes a configurable run-time capability, whichallows specifying support for Ada’s dynamic features in an a la cartefashion ranging from none at all to full Ada. The units included in theexecutable may be either a subset of the standard libraries provided
with GNAT Pro, or specially tailored to the application. This lattercapability is useful, for example, if one of the predefined profiles
implements almost all the dynamic functionality needed in an existing
system that has to meet new safety-critical requirements, and where thecosts of adapting the application without the additional run-time support
are considered prohibitive.

3.3.3.

Full Ada 83 to 2012 Implementation

GNAT Pro provides a complete implementation of the Ada language
from Ada 83 to Ada 2012. Developers of safety-critical and highsecurity systems can thus take advantage of features such as contractbased programming.

3.3.4.

Source to Object Traceability

A compiler option can limit the use of language constructs that generate
object code that is not directly traceable to the source code. As an add30

Frédéric Pothon & Quentin Ochemon service, AdaCore can perform an analysis that demonstrates thistraceability and justifies any remaining cases of non-traceable code.

3.3.5.

Safety-Critical Support and Expertise

At the heart of every AdaCore subscription are the support services that
AdaCore provides to its customers. AdaCore staff are recognized expertson the Ada language, software certification standards in several domains,compilation technologies, and static and dynamic verification. They haveextensive experience in supporting customers in avionics, railway, space,energy, air traffic management/control, and military projects.
Every AdaCore product comes with front-line support provided directlyby these experts, who are also the developers of the technology. This
ensures that customers’ questions (requests for guidance on feature usage,
suggestions for technology enhancements, or defect reports) are handled
efficiently and effectively.
Beyond this bundled support, AdaCore also provides Ada language andtool training as well as on-site consulting on topics such as how to best
deploy the technology, and assistance on start-up issues. On-demand tool
development or ports to new platforms are also available.

3.4. CodePeer
CodePeer is an Ada source code analyzer that detects run-time and logic
errors. It assesses potential bugs before program execution, serving as an
automated peer reviewer, helping to find errors efficiently and early inthe development life-cycle. It can also be used to perform impact analysis
when introducing changes to the existing code, as well as helping
vulnerability analysis. Using control-flow, data-flow, and other advanced
static analysis techniques, CodePeer detects errors that would otherwise
only be found through labor-intensive debugging.

3.4.1.

Early Error Detection

CodePeer’s advanced static error detection finds bugs in programs
before programs are run. By mathematically analyzing every line ofcode, considering every possible input, and every path through theprogram, CodePeer can be used very early in the development life-cycle
31

AdaCore Technologies for DO-178C / ED-12C

to identify problems when defects are much less costly to repair. It canalso be used retrospectively on existing code bases, to detect latentvulnerabilities.
CodePeer is a standalone tool that may be used with any Ada compiler
or fully integrated into the GNAT Pro development environment. It can
detect several of the “Top 25 Most Dangerous Software Errors” in the
Common Weakness Enumeration: CWE-120 (Classic Buffer Overflow),
CWE-131 (Incorrect Calculation of Buffer Size), and CWE-190 (Integer
Overflow or Wraparound). See [7] for more details.

3.4.2.
Qualified for usage in Safety-CriticalIndustries
CodePeer has been qualified as a Verification Tool under DO-178B/ED12B, automating a number of activities associated with that standard’s
objectives for software accuracy and consistency.
Qualification material for both DO-178B/ED-12B and DO-178C/ED-12C
is available as a product option.

3.5. Basic Static Analysis tools
3.5.1.

ASIS, GNAT2XML

ASIS, the Ada Semantic Interface Specification, is a library that gives
applications access to the complete syntactic and semantic structure of an
Ada compilation unit. This library is typically used by tools that need toperform some sort of static analysis on an Ada program.
ASIS is an international standard (ISO/IEC 15291:1995) and is designed
to be compiler independent. Thus a tool that processes the ASIS
representation of a program will work regardless of which ASIS
implementation has been used. ASIS-for-GNAT is AdaCore’s
implementation of the ASIS standard, for use with the GNAT Pro Ada
development environment and toolset.
AdaCore can assist customers in developing ASIS-based tools to meettheir specific needs, as well as develop such tools upon request.

32

Frédéric Pothon & Quentin Ochem

Typical ASIS-for-GNAT applications include:

Static analysis (property verification)

Code instrumentationDesign and document generation tools



Metric testing or timing Tools



Dependency tree analysis tools

Type dictionary generatorsCoding standard enforcement tools

Language translators (e.g., to CORBA IDL)

Quality assessment toolsSource browsers and formatters



Syntax directed editors

GNAT2XML provides the same information as ASIS, but allows users tomanipulate it through an XML tree.

3.5.2.

GNATmetric

The GNATmetric tool analyzes source code to calculate a set of commonlyused industry metrics, thus allowing developers to estimate the size andbetter understand the structure of the source code. This information also
facilitates satisfying the requirements of certain software development
frameworks.

3.5.3.

GNATcheck

GNATcheck is a coding standard verification tool that is extensible andrule-based. It allows developers to completely define a coding standard
as a set of rules, for example a subset of permitted language features. It
verifies a program’s conformance with the resulting rules and thereby

33

AdaCore Technologies for DO-178C / ED-12C

facilitates demonstration of a system’s compliance with certification
standards such as DO-178B / ED-12B and DO-178C / ED-12C.
Key features include:

An integrated Ada Restrictions mechanism for banning specificfeatures from an application. This can be used to restrict features
such as tasking, exceptions, dynamic allocation, fixed- or floating
point, input/output and unchecked conversions.



Restrictions specific to GNAT Pro, such as banning features that
result in the generation of implicit loops or conditionals in theobject code, or in the generation of elaboration code.

Additional Ada semantic rules resulting from customer input, suchas ordering of parameters, normalized naming of entities, andsubprograms with multiple returns.

Easy-to-use interface for creating and using a complete coding
standard.



Generation of project-wide reports, including evidence of thelevel of compliance with a given coding standard.

Over 30 compile-time warnings from GNAT Pro that detect
typical error situations, such as local variables being used before
being initialized, incorrect assumptions about array lower bounds,
infinite recursion, incorrect data alignment, and accidental hidingof names.



Style checks that allow developers to control indentation, casing,comment style, and nesting level.

3.5.4.

GNATstack

GNATstack is a software analysis tool that enables Ada/C softwaredevelopment teams to accurately predict the maximum size of thememory stack required to execute an embedded software application.
The GNATstack tool statically predicts the maximum stack space requiredby each task in an application. The computed bounds can be used to34

Frédéric Pothon & Quentin Ochem

ensure that sufficient space is reserved, thus guaranteeing safe execution
with respect to stack usage. The tool uses a conservative analysis to deal
with complexities such as subprogram recursion, while avoiding
unnecessarily pessimistic estimates.
This static stack analysis tool exploits data generated by the compiler tocompute worst-case stack requirements. It performs per-subprogram stackusage computation combined with control flow analysis.
GNATstack can analyze object-oriented applications, automaticallydetermining maximum stack usage on code that uses dynamic dispatchingin Ada. A dispatching call challenges static analysis because the identityof the subprogram being invoked is not known until run time. GNATstacksolves this problem by statically determining the subset of potential
targets (primitive operations) for every dispatching call. This significantly
reduces the analysis effort and yields precise stack usage bounds oncomplex Ada code.
This is a static analysis tool in the sense that its computation is based on
information known at compile time. When the tool indicates that the result
is accurate, the computed bound can never be exceeded.
On the other hand, there may be cases in which the results will not be
accurate (the tool will report such situations) because of some missing
information (such as the maximum depth of subprogram recursion, indirectcalls, etc.). The user can assist the tool by specifying missing call graphand stack usage information.
GNATstack’s main output is the worst-case stack usage for every entry
point, together with the paths that result in these stack sizes. The list ofentry points can be automatically computed (all the tasks, including theenvironment task) or can be specified by the user (a list of entry points or
all the subprograms matching a given regular expression).
GNATstack can also detect and display a list of potential problems when
computing stack requirements:Indirect (including dispatching) calls. The tool will indicate thenumber of indirect calls made from any subprogram.

35

AdaCore Technologies for DO-178C / ED-12C



External calls. The tool displays all the subprograms that arereachable from any entry point for which there is no stack or callgraph information.

Unbounded frames. The tool displays all the subprograms thatare reachable from any entry point with an unbounded stackrequirement. The required stack size depends on the arguments
passed to the subprogram. For example:
procedure P(N : Integer) is
S : String (1..N);
begin
...
end P;



Cycles. The tool can detect all the cycles (i.e., potentialrecursion) in the call graph.

GNATstack allows the user to supply a text file with the missing
information, such as the potential targets for indirect calls, the stackrequirements for externals calls, and the maximal size for unboundedframes.

3.6. Dynamic Analysis Tools
3.6.1.

GNATtest

The GNATtest tool helps create and maintain a complete unit testing
infrastructure for complex projects. Based on AUnit, it captures the simple
idea that each visible subprogram should have at least one
corresponding unit test. GNATtest takes a project file as input, andproduces two outputs:

36



The complete harnessing code for executing all the unit tests
under consideration. This code is generated completely
automatically.



A set of separate test stubs for each subprogram to be tested.
These test stubs are to be completed by the user.

Frédéric Pothon & Quentin Ochem

GNATtest handles Ada’s Object-Oriented Programming features and canbe used to help verify tagged type substitutability (the Liskov Substitution
Principle) that can be used to demonstrate consistency of class hierarchies.

3.6.2.

GNATemulator

GNATemulator is an efficient and flexible tool that provides integrated,
lightweight target emulation.
Based on the QEMU technology, a generic and open-source machineemulator and virtualizer, GNATemulator allows software developers tocompile code directly for their target architecture and run it on their hostplatform, through an approach that translates from the target object code
to native instructions on the host. This avoids the inconvenience and cost of
managing an actual board, while offering an efficient testing environment
compatible with the final hardware.
There are two basic types of emulators. The first can serve as a surrogate
for the final hardware during development for a wide range ofverification activities, particularly those that require time accuracy.
However, they tend to be extremely costly, and are often very slow. The
second, which includes GNATemulator, does not attempt to be a complete
time-accurate target board simulator, and thus it cannot be used for all
aspects of testing. But it does provide a very efficient and cost-effective
way to execute the target code very early in the development andverification processes. GNATemulator thus offers a practical compromise
between a native environment that lacks target emulation capability, anda cross configuration where the final target hardware might not be
available soon enough or in sufficient quantity.

3.6.3.

GNATcoverage

GNATcoverage is a dynamic analysis tool that analyzes and reports
program coverage. GNATcoverage can perform coverage analysis at
both the object code level (instruction and branch coverage), and thesource code level for Ada or C (Statement, Decision, and Modified
Condition/Decision Coverage - MC/DC).
Unlike most other technologies, GNATcoverage is nonintrusive: it works
without requiring instrumentation of the application code. Instead, the37

AdaCore Technologies for DO-178C / ED-12C

code runs directly on an instrumented execution platform, such as
GNATemulator, Valgrind on Linux, or on a real board monitored by aprobe.
See [8] for more details on the underlying technology.

3.7. Integrated Development Environments(IDEs)
3.7.1.

GNAT Programming Studio (GPS)GPS is a powerful and simple-to-use IDE that streamlines softwaredevelopment from the initial coding stage through testing, debugging,system integration, and maintenance. GPS is designed to allow
programmers to get the most out of GNAT Pro technology.
Tools
GPS’s extensive navigation and analysis tools can generate a variety ofuseful information including call graphs, source dependencies, project
organization, and complexity metrics, giving a thorough understanding ofa program at multiple levels. It allows interfacing with third-party Version
Control Systems, easing both development and maintenance.
Robust, Flexible and Extensible
Especially suited for large, complex systems, GPS can import existing
projects from other Ada implementations while adhering to their filenaming conventions and retaining the existing directory organization.
Through the multi-language capabilities of GPS, components written in C
and C++ can also be handled. GPS is highly extensible; additional tools
can be plugged in through a simple scripting approach. It is also
tailorable, allowing various aspects of the program’s appearance to becustomized in the editor.
Easy to learn, easy to use
GPS is intuitive to new users thanks to its menu-driven interface withextensive online help (including documentation on all the menu selections)and “tool tips”. The Project Wizard makes it simple to get started,
supplying default values for almost all of the project properties. For
experienced users, GPS offers the necessary level of control for

38

Frédéric Pothon & Quentin Ochem

advanced purposes; e.g., the ability to run command scripts. Anything thatcan be done on the command line is achievable through the menu
interface.
Remote Programming
Integrated into GPS, Remote Programming provides a secure andefficient way for programmers to access any number of remote servers on
a wide variety of platforms while taking advantage of the power andfamiliarity of their local PC workstations.

3.7.2.

Eclipse support - GNATbench

GNATbench is an Ada development plug-in for Eclipse and Wind River’s
Workbench environment. The Workbench integration supports Ada
development on a variety of VxWorks real-time operating systems. The
Eclipse version is primarily for native applications, with some support forcross development. In both cases the Ada tools are tightly integrated.

3.7.3.

GNATdashboard

GNATdashboard serves as a one-stop control panel for monitoring andimproving the quality of Ada software. It integrates and aggregates theresults of AdaCore’s various static and dynamic analysis tools(GNATmetric, GNATcheck, GNATcoverage, CodePeer, SPARK Pro, among
others) within a common interface, helping quality assurance managers
and project leaders understand or reduce their software’s technical debt,
and eliminating the need for manual input.
GNATdashboard fits naturally into a continuous integration environment,
providing users with metrics on code complexity, code coverage,
conformance to coding standards, and more.

3.8. Model-Based Development: QGen
QGen is a qualifiable and tunable code generation and model
verification tool for a safe subset of Simulink® and Stateflow® models. It
reduces the development and verification costs for safety- criticalapplications through qualifiable code generation, model verification, andtight integration with AdaCore’s qualifiable simulation and structural
coverage analysis tools.

39

AdaCore Technologies for DO-178C / ED-12C

QGen addresses one core issue: how to decrease the verification costs on
the model and the code when applying model-based design andautomatic code generation with the Simulink® and Stateflow®
environments. QGen achieves this by

Enforcing a safe subset of Simulink® blocks



Providing high-performance and tunable code generationPerforming static analysis for upfront detection of potential
errors, and

Making available DO-178B/ED-12B and DO-178C/ED-12CC
qualification material for both the code generator and the model
verification tools. QGen can also integrate smoothly with
AdaCore’s qualifiable simulation and structural coverage analysis
tools.

3.8.1.
Support for Simulink® and Stateflow®
models
QGen supports a wide range of features from the Simulink® andStatefow® environments, including more than one hundred blocks,
Simulink® signals and parameters objects, and several Matlab®
operations. The supported feature set from the Simulink® and Stateflow®
environments has been carefully selected to ensure code generation thatis amenable to safety-critical systems. MISRA-C Simulink® constraints canbe optionally checked with QGen. Features that would imply
unpredictable behavior, or that would lead to the generation of unsafe
code, have been removed. The modelling standard enforced by QGen isthen suitable for DO-178/EN-12(B/C), CENELEC EN 50128 and ISO
26262 development out-of-the-box.

3.8.2.

Qualification material

Qualification for QGen will demonstrate compliance with the DO-178C /ED-12C standard at Tool Qualification Level 1 (TQL-1, equivalent to a
Development Tool in DO-178B / ED-12B), making QGen the only code
generator for Simulink® and Stateflow® models for which a TQL-1

40

Frédéric Pothon & Quentin Ochem

qualification kit is available. The QGen qualification kit will showcompliance with DO-330 / ED-215 (Tool Qualification Considerations)and include a Tool Qualification Plan, a Tool Development Plan, a Tool
Verification Plan, a Tool Quality Assurance Plan and a Tool Configuration
Management Plan. It will also include detailed Tool Operational
Requirements, Tool Requirements, Test Cases and Test Execution Results,
together with a Tool Configuration Index and a Tool Accomplishment
Summary.

3.8.3.

Support for model static analysis

QGen supports static verification that three kinds of defects areprevented: run-time errors, logical errors, and safety violations. Run-timeerrors, such as division by zero or integer overflow, may lead to
exceptions being raised during software execution. Logical errors, forexample a Simulink® “If” block condition that is always True, imply adefect in the designed model. And safety properties, which can bemodeled using Simulink® Model Verification blocks, represent safety
requirements that are embedded in the design model. QGen is able tostatically verify all these properties and generate run-time checks as well
if configured to do so.

3.8.4.
Support for Processor-in-the-Loop
testing
QGen can be integrated with AdaCore’s GNATemulator and
GNATcoverage tools to support streamlined Processor-In- the-Loop (PIL)
testing. The simulation of Simulink® models can be tested back-to-backagainst the generated code, which is cross-compiled and deployed on a
GNATemulator installation on the user workstation. While conducting PIL
testing, GNATcoverage can also perform structural coverage analysis up
to MC/DC without any code instrumentation. Both GNATcoverage and
GNATemulator have already been qualified in an operational context.

41

AdaCore Technologies for DO-178C / ED-12C

4. Compliance with DO178C / ED-12C Guidance:
Analysis4.1. Overview
DO-178C / ED-12C uses the term “requirement” to identify the expectedbehavior of the system, the software, or a part thereof. The desired
functions are formulated at the system level as “system requirements” andare refined and elaborated into “software requirements”. DO-178C /ED-12C identifies several categories of software requirements.
The High-Level Requirements (HLR) define the expected behavior of thecomplete software loaded on the target computer, independent of thesoftware architecture. The HLR are further refined into one or more lower
levels, specifying the expected behavior of each software subpart(component) based on the architecture definition. The lowest level ofrequirements (the LLR) and the architecture are translated into source
code, which finally is compiled to produce the Executable Object Code
(EOC).
Within this basic framework, the development process activities(requirements definition, design, coding, and integration) should be
conducted so as to reduce the likelihood of introducing errors. Verification
process activities are designed to detect errors through multiple filters, byassessing the same artifacts in different ways. This naturally applies to the
EOC, whose verification involves checking compliance with therequirements at each level, using both normal and abnormal inputs. Such
verification is typically performed by testing. Finally, the EOC verificationmust itself be verified.
While it is not a DO-178C / ED-12C concept, a “V” cycle is often used torepresent the complete software life cycle. A variation of the traditional“V” cycle, oriented around the DO-178C / ED-12C processes, was shown

42

Frédéric Pothon & Quentin Ochem

earlier in Figure 1. As is seen in that figure, AdaCore tools mostly apply
towards the bottom stages of the “V” cycle:

Design (architecture + LLR), coding and integration (EOC
generation), for the development activities.

Design and source code review / analysis and LLR testing, for theverification activities.

Additional support is provided for design activities in conjunction with thethree technology supplements (on model-based development, objectoriented technology, and formal methods).
The core element of the AdaCore tool chain is a development
environment, including a compiler for Ada and C. Complementary tools
support several verification activities, such as GNATcheck for code
standard checking, CodePeer for static analysis, GNATstack for stackchecking, and GNATtest / GNATcoverage for testing and structural code
coverage analysis.
To show how AdaCore tools can be used in connection with the software
life cycle processes for a system that is to be assessed against DO-178C/ ED-12C, several possible scenarios will be described:


Use Case 1: Traditional development process, excluding or
including OOT
The development process produces requirements specified in text
(natural language) that are implemented in Ada source code. A
code standard defines a set of restrictions, which may or may notinclude limitations on object-oriented features. Both cases need tobe considered:o

Use Case 1a: No use is made of object oriented
technology or related techniqueso

Use Case 1b: Ada’s OOT features are used, and theguidance in DO-332 / ED-217 is considered

43

AdaCore Technologies for DO-178C / ED-12C



Use Case 2: Model-Based Development
The development process includes a design model, which is
automatically translated into MISRA-C or SPARK/Ada by aqualified code generator such as provided in QGen. The
certification effort follows the additional guidance from theModel-Based Development supplement (DO-331 / ED-218) andthe Tool Qualification Considerations standard (DO-330 / ED215), to obtain certification credit for using a qualified code
generator.



Use Case 3: Formal Methods
The development uses a formal description of the low-level
requirements, namely SPARK / Ada 2012 contracts. A formal
analysis is performed, and credit is claimed on reducing thetesting. The certification effort follows the additional guidancefrom the Formal Methods Supplement (DO-333 / ED-216).

In the tables that appear in this chapter, the references shown inparentheses for the objectives identify the table, objective number, andparagraph reference for the objective in the DO-178C / ED-12C
standard or the relevant technology supplement. For example, A-2[6]:5.3.1.a refers to Table A-2, Objective 6, paragraph 5.3.1a.

44

Frédéric Pothon & Quentin Ochem

4.2. Use case #1a: Coding with Ada 2012
The adoption of Ada as the coding language brings a number of benefits
during design, coding, and testing, both from language features (assummarized in the table below) and from the AdaCore ecosystem.

4.2.1.

Benefits of the Ada language
Contributions

Objectives

Software Coding (A-2[6]: 5.3.1.a)
Reviews and Analyses of Source Code:- Verifiability (A-5[3]- 6.3.4.c)- Accuracy and consistency (A-5[6]- 6.3.4.f)

Activities

Software Coding (5.3.2.a)
Reviews and Analyses of Source Code (6.3.4)

Ada’s most significant contribution is towards the reliability of the written
code; the language is designed to promote readability andmaintainability, and to detect errors early in the software development
process. This section will summarize several Ada features that help meetthese goals.
Strong typing
The emphasis on early error detection and program clarity is perhaps
most clearly illustrated in the language’s “strong typing”. A type in Ada isa semantic entity that can embody static (and possibly also dynamic)
constraints. For example:
type Ratio is digits 16 range -1.0 .. 1.0;

In the above example, Ratio is a floating-point type. Two constraints are
specified:

digits specifies the minimum precision needed for objects of thistype, in terms of decimal digits. Here the compiler will likely
choose a 64-bit representation. If the target architecture only45

AdaCore Technologies for DO-178C / ED-12C

supports 32-bit floating-point, the compiler will reject the
program.
range defines the set of acceptable values. Here, only values

between -1.0 and 1.0 are acceptable; an attempt to assign avalue outside this range to a variable of type Ratio will raise arun-time exception (Constraint_Error).
Strong typing means an absence of implicit conversions (implicit “casts”),
since such conversions can mask logical errors. For example:
type Miles
is digits 16;
type Kilometers is digits 16;...
Distance_1 : Miles;
Distance_2 : Kilometers;...
Distance_1 := Distance_2; -- Illegal, rejected at compile time

Both Miles and Kilometers are 16-digit floating-point types (therange constraint is optional in a floating-point type declaration) but they
are different types, and thus the assignment is illegal. Likewise, it is illegal
to combine Miles and Kilometers in an expression; Miles + Kilometers
would also be rejected by the compiler.
With strong typing the program’s data can be partitioned so that an
object of a given type can only be processed using operations that makesense for that type. This helps prevent data mismatch errors.
Explicit conversions between related types are allowed, either
predefined (for example between any two numeric types) or supplied by
the programmer. Explicit conversions make the programmer’s intent clear.
For example:

46

Frédéric Pothon & Quentin Ochem

type Grade is range 0..100;-- a new integer type

Test_Grade : Grade;N: Integer;-- predefined type...
Test_Grade := N;-- Illegal (type mismatch), rejected at compile time
Test_Grade := Grade (N);-- Legal, with run-time constraint check that N is in 0..100

Dimensionality checking
One of the challenges to a language’s type model is the enforcement of
the proper use of units of measurement. For example dividing a distanceby a time should be allowed, yielding a velocity. But the error of dividing
a time by a distance where a velocity value is required should be
detected and reported as an error at compile time.
Although this issue could be addressed in theory by defining a separate
type for each unit of measurement, such an approach would require
defining functions (likely as overloaded operator symbols) for thepermitted operand combinations. This would be notationally cumbersome
and probably not used much in practice.
The GNAT Pro environment provides a solution through theimplementation-defined aspects Dimension_System which can beapplied to a type, and Dimension which can be applied to a subtype.
Uses of variables are checked at compile time for consistency based on
the Dimension aspect of their subtypes. The GNAT library includes a
package System.Dim.Mks that defines a type and its associatedsubtypes that will be used for meters (Length), kilograms (Mass), seconds(Time), and other units. The programmer can define a subtype such as
Velocity that corresponds to Length (in meters) divided by Time (inseconds):47

AdaCore Technologies for DO-178C / ED-12C

subtype Velocity is Mks_Type with
Dimension => ("m/sec",
Meter => 1,-- Values are exponents in the product of-- the units
Second => -1,
others => 0);

With such a declaration the following is permitted:
My_Distance : Length
My_Time: TimeMy_Velocity : Velocity:= 10 * m;:= 5.0 * h;-- m is 1.0 meter-- h is 1.0 hour-- (3600.0 sec):= My_Distance / My_Time; -- OK

A Velocity value should be computed as a distance divided by a time.
The following will be detected as an error:
My_Distance : Length
My_Time: TimeMy_Velocity : Velocity:= 10 * m;:= 5.0 * h;:= My_Time / My_Distance;-- Illegal

GNAT Pro’s support for dimensionality checking is a useful adjunct to
Ada’s strong typing facilities.
Pointers
For compliance with DO-178C/ED-12C, the use of dynamic memory (andpointers) should be kept to the bare minimum, and Ada helps support thisgoal. Features such as arrays or by-reference parameter passing, which
require pointers or explicit references in other languages, are captured
by specific facilities in Ada. For example, Ada’s parameter passing
mechanism reflects the direction of data flow (in, out, or in out) rather
than the implementation technique. Some data types always require bycopy (for example scalars), and some types always require by-reference(for example tagged types, in OOP). For all other types the compiler will
choose whether it is more efficient to use by-reference (via a hidden
pointer or reference) or by-copy. Since the developer does not have to
explicitly manipulate pointers to obtain by-reference passing, many
common errors are avoided. Here’s an example:

48

Frédéric Pothon & Quentin Ochem

type Rec isrecordA, B : Integer;
end record;
My_Rec : Rec;
procedure Update (R : in out Rec);...
Update (My_Rec);The above procedure takes a Rec object as an in out parameter. In the
invocation Update (My_Rec), the compiler may choose to pass My_Rec
either by reference or by copy based on efficiency considerations. In
other languages the programmer would need to use pointers to obtainby-reference passing if the actual parameter needs to be modified by
the called subprogram.
When pointers are absolutely required, Ada’s approach is to supply a
type-safe and high-level mechanism (known as “access types”) to obtainthe needed functionality while also providing low-level facilities that arepotentially unsafe but whose usage is always explicitly indicated in thesource text (thus alerting the human reader). To illustrate this, here’s a C
code fragment that performs pointer arithmetic:
int *ptr = malloc (sizeof (int));
ptr++;

This may or may not be safe; after the increment, ptr points to a location
immediately beyond the storage for the allocated int.
As part of its C interfacing facilities Ada supports such pointer arithmetic,
indeed with algorithmic code that is similar to the C notation, but thedependence on a potentially unsafe operation is explicit:

49

AdaCore Technologies for DO-178C / ED-12C

with Interfaces.C.Pointers;
procedure Pointer_Arith istype Int_Array isarray (Positive range <>) of aliased Integer;
package P is
new Interfaces.C.Pointers(Positive, Integer,
Int_Array, Integer'First);-- This generic instantiation defines the access type-- Pointer and its associated operations
use type P.Pointer;-- For notational convenience in invoking "+"Ref : P.Pointer := new Integer;
begin
Ref := Ref+1;-- Increments Ref by the size (number of storage elements)-- of an Integer
end Pointer_Arith;

This syntax, though verbose, makes potentially unsafe operations much
more visible, hence easier to identify and review.
Arrays
The array (an indexable sequence of elements) is a fundamental andefficient data structuring mechanism, but a major vulnerability unlessattempted accesses to data outside the bounds of the array areprevented. Ada avoids this vulnerability since array operations such asindexing are checked to ensure that they are within the specified bounds.
In addition to indexing, Ada provides various array operations(assignment, comparison, slicing, catenation, etc.) which allow manipulatingarrays in an explicit and safe manner.
Ada’s arrays are “fixed size”; once an array object is created, its bounds
are established and cannot change. This simplifies the storage
management (arrays in Ada can go on the stack and do not require
hidden pointers). Additional flexibility (for example bounded-size arrays
whose length can vary up to a specified maximum limit, or unboundedarrays of arbitrary length) is obtained through the Ada predefined
library.

50

Frédéric Pothon & Quentin Ochem

Here’s an example:
type Int_Array is array(Positive range <>) of Integer;-- Different objecTs of type Int_Array can have different-- bounds
A : Int_Array (1 .. 8);
B : Int_Array (2 .. 12);I : Integer;...
A := (others => 0);
B := (2 .. 7 => 0, others => 1);...
if A (1 .. 3) = B (6 .. 8) then
Put_Line ("Slices are equal");end if;Get (I);
A (I) := 100;-- Read in an integer-- Run-time check that I is in range

The above code creates two arrays, A with 8 elements indexed from 1 to8, and B with 11 elements indexed from 2 to 12. A is assigned all zeroes,
and B is assigned 0 in its first 6 elements and 1 in the rest. Contiguous
sequences (slices) of the two arrays are compared for equality. All of thisis done through standard language syntax as opposed to explicit loops
or library calls.
The code at the end of the example illustrates Ada’s index checking. If I
is not in the index range of array A (i.e., between 1 and 8 inclusive) thena run-time exception (Constraint_Error) is raised.
Other Ada features
Many other features contribute to Ada’s support for reliable andmaintainable embedded software. Some were described briefly in
Section 3.1.1. Others include the Ravenscar Profile, a deterministic tasking
subset that is simple enough for certification but rich enough to program
real-time embedded systems; and Ada’s low-level facilities, which allow
the programmer to specify target-specific representations for data types(including the bit layout of fields in a record, and the values for

51

AdaCore Technologies for DO-178C / ED-12C

enumeration elements). Further information on features that contribute tosafe software may be found in [3].
In summary, Ada’s benefits stem from its expressive power, allowing thedeveloper to specify the needed functionality or to constrain the feature
usage to a deterministic subset, together with its support for reliability
and readability. A variety of errors, including some of the most frequentand harmful vulnerabilities, are detected in Ada either at compilation
time or through dynamic checks automatically added by the compiler.
Such checks can be either retained (for example during a testing
campaign) or removed (for example at production time, after verification
has provided confidence that they are not needed).
Additional Ada features will be described and highlighted in othersections of this document.

4.2.2.

Using Ada during the design process
Contributions

Objectives

Software Design Process (A-2[3,4]: 5.2.1.a)
Reviews and Analyses of Source Code: Compliance witharchitecture (A-5[2]: 6.3.4.b), traceability (A-5[5]:6.3.4.e)
Reviews and Analyses of LLR: Compatibility with target (A5[3]: 6.3.2.c)
Reviews and Analyses of architecture: Compatibility withtarget (A-4[10]: 6.3.3.c)

Activities

Software Design Activities (5.2.2.a, 5.2.2.d)
Software Development Process Traceability (5.5.c)
Reviews and Analyses of Source Code (6.3.4)
Reviews and Analyses of LLR: Compatibility with target(6.3.2)
Reviews and Analyses of architecture: Compatibility withtarget (6.3.3)

An application’s design – that, its low-level requirements and softwarearchitecture – may be specified in many ways, combining text andgraphics at various levels of formality. The main principle is to keep thedesign at a higher level of abstraction than the code: in particular
avoiding expression of requirements as code or pseudo-code.

52

Frédéric Pothon & Quentin Ochem

Requirements are properties to be verified by the code and are not thecode itself. Thus the general advice is to avoid using a programming
language as the medium for expressing – even in part – the software
design.
Ada, however, presents an exception to this advice. The language
provides extensive facilities for capturing a program unit’s specification (its“what”) separately from the implementation (its “how”). An Ada package
and an Ada subprogram each consists of a specification (the interface)and a body (the implementation) and a similar separation of interface
from implementation is found in generic units, tasks, and encapsulated
types.
A unit’s specification establishes the constraints on its usage, that is, thepermitted relationships between that unit and other parts of the program.
These are the unit’s architectural properties, in contrast to its
implementation. It thus makes sense for a significant part of the Ada
specifications to be developed during the design process. An interesting
effect is that the design elements defined as Ada specifications are easy
to verify, sometimes simply by compiling the code and showing that theinterface usages are correct.
The separation of specification and implementation means that an Ada
specification can have an implementation written in a different language,
for example C. Although this may lose some of Ada’s benefits, it illustrates
the flexibility and relevance of the approach.

4.2.2.1 Component identification
Regardless of the method used for architecting the software as ahierarchical set of components, Ada may be directly used to identify thesoftware components and define their interfaces. This is typically done via
package specifications and subprogram specifications.
A few comments on the term “interface” may be helpful. (We are notreferring to the OOP language feature here.) Informally, a component’s
interface is the collection of its properties that establish whether any given
usage of the component is correct. These properties arise at several
levels. As an example, for a procedure that sorts an array of floating
point values its interface may be regarded as comprising the following:

53

AdaCore Technologies for DO-178C / ED-12C



Syntactic interface: the procedure’s name and its formal
parameters (their names, parameter passing modes, and types).

Information flow interface: how, if at all, non-local data areaccessed by the procedure (read, written, or both)

Semantic (functional) interface: the function performed by theprocedure – what does it mean to sort an array, independent of
the algorithm – which is a low-level requirement for theprocedure

Other low-level constraints may also be considered as part of theinterface, such as a time or space constraint.
The syntactic interface in Ada is a simple subprogram specification:
type Float_Array is array (Integer range <>) of Float;
procedure Sort (My_Array : in out Float_Array);This will also suffice for information flow if Sort does not access non-local
data. If Sort does access non-local data then the uses can be specified
informally by comments:
type Float_Array is array (Positive range <>) of Float;
procedure Sort (My_Array : in out Float_Array);-- Inputs: None-- Outputs-- p_GLOBAL.Status : p_GLOBAL.T_Status;

They can also be captured more formally as aspects of the procedure
specification if the SPARK subset of Ada is used, as will be explained
below.
The LLR (including the semantic interface) are developed in parallel andmay be specified separately from or together with the component’s
specification. They can be defined in natural language, as comments, or54

Frédéric Pothon & Quentin Ochem

using contracts (pre- and/or postconditions) as illustrated in the next
subsection.

4.2.2.2. Low-Level Requirements
A simple example of a low-level requirement, for the Sort proceduredefined above, is the following:
The component shall order the array from the smallest value tohighest one
In Ada, we can capture this requirement as a postcondition aspect of theprocedure:
type Some_Array is array (Positive range <>) of Integer;
procedure Sort (My_Array : in out Some_Array)with Post =>(for all I in My_Array'First .. My_Array'Last-1 =>My_Array (I) <= My_Array (I+1) );The with Post construct defines the postcondition for the procedure; i.e.,the condition that is asserted to be True when the procedure returns. Hereit expresses, in Ada syntax, the low-level requirement that the procedure
sort the array in ascending order: for each index I into the array, fromthe first position through the next-to-last, the value of the element at
position I+1 is at least as large as the element at position I. In thedegenerate case where the array is either empty or contains a single
element (i.e., when the range of I is empty) the “for all” condition isconsidered to be True.
It’s clear that the postcondition expression says nothing about how theprocedure is implemented. It’s not pseudo-code for an algorithm but
rather a property of the procedure that will need to be verified. It’s theformalization of a requirement that happens to use Ada syntax.
Moreover, a postcondition can refer to the values of variables and/or
global data, both at the point of call and the point of return, and afunction postcondition can refer to the value being returned by thefunction.

55

AdaCore Technologies for DO-178C / ED-12C

A subprogram can also have a precondition (a Boolean expression), which
is a requirement that the caller needs to satisfy and that is assumed to be
True by the called subprogram. For example, a procedure that inserts anelement into a bounded-length data structure would have a precondition
asserting that the data structure is not full.
Preconditions and postconditions, and related features such as typeinvariants, are referred to collectively as contract-based
programming and were introduced in the Ada 2012 version of thelanguage. Based on the assertion policy (as specified by a pragma), thecontracts can be checked at run-time, raising an exception on failure.
They also support (but do not require) formal analysis, since the Ada
syntax is the same as is used in SPARK 2014. In SPARK the contracts are
subject to additional restrictions (for example they must conform to theSPARK language subset). The contracts are then considered to be lowlevel requirements and verification cases at the same time, used by theSPARK proof technology for formal verification, for example todemonstrate that if a subprogram satisfies its precondition then on return
it will satisfy its postcondition.
In summary, functional contracts (such as pre- and postconditions) serve
three purposes:

As conditions to be formally proved by SPARK technology,

As run-time conditions to be evaluated/checked using standard
Ada semantics, andAs comments to the human reader (if checks are not enabled andformal methods are not used) in an unambiguous notation (i.e.,
using Ada syntax rather than natural language)

When used for defining the software’s architecture, Ada specifications
can obviously express concepts such as modules (packages), groups ofmodules (package hierarchies), subprograms, class inheritance hierarchies,
etc. Additional interface properties can be expressed using SPARK
aspects, for example a subprogram’s data and flow dependencies.
Here’s an example which, for simplicity and purposes of illustration, uses
visible variables in a package specification to represent a data structure
for a last-in first-out stack:56

Frédéric Pothon & Quentin Ochem

package Stack_Pkg is
Max_Length : constant := 100;
subtype Element_Type is Integer;
LengthStack: Natural range 0.. Max_Length := 0;: array (1..Max_Length) of Element_Type);

procedure Push ( Item : in Element_Type )with Global => (In_Out => (Length, Stack)),
Depends => (Length => Length,
Stack => (Stack, Length, Item)),Pre=> Length < Max_Length,
Post=> Length = Length'Old+1;...
end Stack_Pkg;

The Global aspect captures the data dependency: Push will reference
and assign to the global variables Length and Stack.
The Depends aspect captures the flow dependency: the new value ofLength depends on its old value, and the new value of Stack depends
on the values of Stack, Length, and Item. These dependencies can beverified by the SPARK tools (assuming that the subprogram body is
written in the SPARK subset). The pre- and postconditions reflect some of
the functional properties of the procedure, and the postcondition
illustrates the 'Old attribute for referencing the point-of-call value of avariable.
A more realistic version of this example would hide the representation in
the private part or body of the package. The contracts would then be
expressed differently, for example with the Global and Depends
referring to the abstract state of the package rather than visible
variables.
Some low-level requirements might not be expressible using the aspectmechanism (for example timing constraints). A convenient approach duringarchitecture definition is to separately specify those components whose
requirements can be defined using contracts, from those that cannot.

57

AdaCore Technologies for DO-178C / ED-12C

4.2.2.3. Implementation of Hardware/Software Interfaces
Ada’s type system makes it straightforward to implement
hardware/software interfaces, while also detecting target
incompatibilities at compile time. Such interfaces may be defined as partof the coding process, but performing this activity during the design
process has a number of benefits. It may avoid duplication of effort andalso helps prevent errors from being introduced during the translationfrom design to code. It also allows early error detection throughcompilation checks.
Package Interfaces

Applications sometimes need to use types that correspond exactly to thenative numeric data representations supported on the target machine, forexample 16- or 32-bit signed and unsigned integers. Such types aredefined in package Interfaces, which is part of the standard Ada library.
The exact set of types depends on the target but typically includes
integer types such as Unsigned_16, Unsigned_32, Integer_16, andInteger_32, as well as several floating-point types. The unsigned integer
types are especially useful for hardware / software interfacing since they
support bitwise operations including shift and rotate functions.
Specifying data representation

Embedded systems often need to deal with external data having a
specific representation, and Ada has a variety of features to help meetthis requirement. For example, the following can be defined:

the values of the elements in an enumeration type,the layout of a record (size and position of each field, possiblywith fields overlaid), andthe address, size, and/or alignment of a data object.

The compiler will check that the specified representation is consistent withthe target hardware.
For example, Figure 3 shows the required layout (on a “little-endian”
machine) for a data object consisting of an unsigned 16-bit integer (Num),
58

Frédéric Pothon & Quentin Ochema 4-bit enumeration value (Urgency) that is either Low, Medium, or High,with the respective values 2, 5, and 10), and a Boolean flag (F).

Figure 3: Data Layout
As with other entities, Ada separates the type’s “interface” (its logicalstructure as a record type with named fields) from its “implementation”(its physical representation / layout including size, alignment, and exact
position of each field). The representation can be specified through a
combination of aspects and representation clauses. Defining the
Bit_Order and the Scalar_Storage_Order explicitly means that thecode will work correctly on both little-endian and big-endian hardware.
type Urgency_Type is (Low, Medium, High);for Urgency_Type use (Low => 2, Medium => 5, High => 10);for Urgency_Type'Size use 4; -- Number of bits

59

AdaCore Technologies for DO-178C / ED-12C

type Message isrecordNum: Interfaces.Unsigned_16;
Urgency : Urgency_Type;F: Boolean;end record
with
Bit_Order=> System.Low_Order_First,
Scalar_Storage_Order => System.Low_Order_First, -- GNATspecifc aspectSize=> 32, -- Bits
Alignment=> 4; -- Storage units
for Message use-- Representation clauserecordNumat 0 range 0..15;
Urgency at 2 range 0..3;
F
at 3 range 2..2;
end record;

The “at” syntax in the record representation clause specifies the offset (instorage units) to the storage unit where the field begins, and the bit
positions that are occupied. A field can overlap multiple storage units.
When the program specifies these kinds of representational details, it’s
typical for the application to read a “raw” value from an external source,
and in such cases it is important to ensure that such data values are valid.
In the above example, the Urgency field needs to have one of thevalues 2, 5, or 10. Any other value has to be detected by the programlogic, and Ada’s 'Valid attribute can perform that check. The following
example illustrates a typical style:
M : Message;...
Device.Read (M); -- Reads a value into M
if not M.Urgency'Valid then... -- Report non-valid input valueelse... -- Normal processing
end if;60

Frédéric Pothon & Quentin Ochem

The 'Valid attribute can be applied to data objects from numeric andenumeration types. It is useful when the permitted values for the object
are a proper subset of the full value set supported by the object’s
representation.
Numeric types
Another feature related to hardware/software interfaces is Ada’snumeric type facility (integer, floating-point, fixed-point). The
programmer can specify the type’s essential properties, such as range
and precision, in a machine-independent fashion; these will be mapped toan efficient data representation, with any incompatibilities detected atcompile time. As an example:
type Nanoseconds is range 0 .. 20_000_000_000;
V : Nanoseconds;

The above code requires integers up to 20 billion to be represented. This
would only be accepted on a 64-bit machine, and the compiler would
reject the program if the target lacks such support. This can even be madeexplicit as part of the type declaration:
type Nanoseconds is range 0 .. 20_000_000_000
with Size => 64;
V : Nanoseconds;

The compiler will check that 64 bits are sufficient, and that it can be
implemented on the target computer.
Similar constraints can be expressed for floating-point types:
type Temperature is digits 14;
V : Temperature;61

AdaCore Technologies for DO-178C / ED-12C

At least 14 digits of decimal precision are required in the representationof Temperature values. The program would be accepted if the target has
a 64-bit floating point unit, and would be rejected otherwise.

4.2.3.

Integration of C components with Ada
Contributions

Objectives

Software Coding (A-2[6]: 5.3.1.a)
Software Integration (A-2[7]: 5.4.1.a)

Activities

Software Coding (5.3.2.a)
Software integration (5.4.2.a)

C is widely used for embedded development, including safety-criticalsystems. Even where Ada is the main language for a system, components
written in C are very commonly included, either from legacy libraries or
third party software. (Languages such as Java and C++ are used muchless frequently. This is due in part to their semantic complexity and the
difficulty of demonstrating compliance with certification standards, forexample for the C++ standard library or the Java Garbage Collector.)
Friendly cooperation between Ada and C is supported in several ways
by AdaCore tools and the Ada language.

62



Most of the tools provided by AdaCore (compiler, debugger,
development environments, etc.) can support systems written
entirely in Ada, in a mixture of Ada and C, and entirely in C.

Specific interfacing tools are available to automatically generatebindings between Ada and C, either creating Ada specificationfrom a C header file (g++ -fdump-ada-spec) or a C header filefrom an Ada specification (gcc -gnatceg). These binding
generators make it straightforward to integrate C components in
an Ada application or vice versa.



The Ada language directly supports interfacing Ada with otherlanguages, most notably C (and also Fortran and COBOL). Oneof the standard libraries is a package Interfaces.C thatdefines Ada types corresponding to the C basic types (int, char,Frédéric Pothon & Quentin Ochemetc.) and implementation advice in the Ada Language Reference
Manual explains how to import C functions and global data to be
used in Ada code, and in the other direction, how to export Ada
subprograms and global data so that they can be used in C.
The GNAT Pro compiler uses the same back end technology forboth Ada and C, facilitating interoperability.



A project using a C codebase can incrementally introduce Ada or
SPARK. Technologies allowing SPARK to specify a component
implemented in C, or compiling SPARK into C code, are underdevelopment [9]. This allows progressive adoption of higher-tierlanguages without losing the investment made in existing
components.

4.2.4.

Robustness / defensive programming
Contributions

Objectives

Software Coding (A-2[6]: 5.3.1.a)
Reviews and Analyses of Source Code: Accuracy andconsistency (A-5[6]: 6.3.4.f)

Activities

Software Coding (5.3.2.b – standards)
Software Coding (5.3.2.c – inadequate/incorrect inputs)
Reviews and Analyses of Source Code (6.3.4)
Robustness Test Cases (6.4.2.2)

Robustness means ensuring correct software behavior in the presence ofabnormal input, and (as per DO-178C / ED-12C) such behavior should
be defined in the software requirements. There is no fundamental
difference between requirements concerning abnormal input (robustness
requirements) and those concerning normal input (functional requirements).
One approach to meeting robustness requirements is through defensive
programming techniques; that is, code that detects incorrect input andperforms the appropriate actions. However, this has two undesirable side
effects.

63

AdaCore Technologies for DO-178C / ED-12C

“Correct behavior in case of incorrect input” is sometimes difficult
to define, resulting in code that cannot be verified byrequirements based tests. Additional test cases based on the code
itself (called “structural testing”) are not acceptable from a DO178C / ED-12C perspective, since they are not appropriate forrevealing errors.



Unexercised defensive code complicates structural coverage
analysis. It can’t be classified as “extraneous” (since it does meeta requirement), but neither can it be considered as “deactivated”(since it is intended to be executed when the input is abnormal).
As with any other non-exercised code, justification should be
provided for defensive code, and this may entail difficult
discussions with certification authorities.

An alternative approach is to ensure that no invalid input is ever supplied(in other words, to make each caller responsible for ensuring that the input
is valid, rather than having the callee deal with potential violations). Thiscan be done through the use of Ada 2012 contracts. Here’s an example,
a procedure that interchanges two elements in an array:
type Float_Array is array (1..100) of Float;
procedure Swap (FA: in out Float_Array;
I1, I2 : in Integer);-- I1 and I2 have to be indices into the array,-- i.e., in FA'Range
procedure Swap (FA: in Float_Array;
I1, I2 : in Integer) is
Temp : Float;
begin
if I1 in FA'Range and then I2 in FA'Range thenTemp:= FA (I1);
FA (I1) := FA (I2);
FA (I2) := Temp;
end if;end Swap;

The above example illustrates the ambiguity of the requirements for
defensive code. What does it mean to invoke Swap when one or both64

Frédéric Pothon & Quentin Ochem

indices are out of range? Not doing anything (which is the effect of theabove code) is a possible answer, but this should be identified as a
derived requirement (since it is an additional behavior of the component).
Other possibilities:

Raise an exceptionReport the error through an additional out parameter to theprocedure, or as a status value returned (if the subprogram wereexpressed as a function rather than a procedure)

Map an out-of-bounds low value to FA'First, and an out-ofbounds high value to FA'Last

Even if one of these options is chosen as the required behavior, there areboth efficiency questions (why should the procedure spend execution timechecking for a condition that is expected to be met) and methodologicalissues with such defensive code.
The responsibility should really be on the caller to avoid invoking theprocedure if any of the actual parameters has an incorrect value. A
comment in the code states that the indexes should be in range, but Ada
2012 allows formalizing this comment in an automatically verifiable way:
type Float_Array is array (Positive range <>) of Float;
procedure Swap (FA : in out Float_Array; I1, I2 : Integer)
with Pre => I1 in FA'Range and then I2 in FA'Range
procedure Swap (FA : in Float_Array; I1, I2 : Integer) is
Temp : Float;
begin
Temp
:= FA (I1);
FA (I1) := FA (I2);
FA (I2) := Temp;
end Swap;

The comment has been replaced by a precondition, which is part of theprocedure specification. Assuming proper verification at each call site,
defensive code in the implementation of the procedure is not needed. The
requirement is now to check that the values passed at each call meet the65

AdaCore Technologies for DO-178C / ED-12C

precondition, and to take appropriate action if not. This action may differ
from call to call, and may involve further preconditions to be definedhigher up in the call chain.
Enforcement of these preconditions may be accomplished through several
possible activities:

66

Code reviews using the Ada contracts as constraints. This is least
formal technique, but the explicit specification of thepreconditions in Ada contract syntax (versus comments) helps
improve the thoroughness of the review and avoids the potential
ambiguity of requirements expressed in natural language.



Enabling dynamic checks during testing, and removing them in the
final executable object code. Run-time checks are generated forpre- and postconditions if the program specifies
pragma Assertion_Policy (Check) and the code is compiled
with the compiler switch -gnata. A violation of a pre- or
postcondition will then raise the Assertion_Error exception.
After testing and related verification activities achieve sufficientassurance that no violations will occur, the checking code can beremoved (either by pragma Asserion_Policy(Ignore) or bycompiling without -gnata).

Enabling dynamic checks during testing, and keeping them in the
final executable object code. In this case, the software
requirements should define the expected behavior in case a preor postcondition is violated, for example to reset the application
to a known safe state as soon as an inconsistency is detected.



Static analysis or formal proof. The CodePeer technology takes
preconditions into account as part of its analysis. The tool canstatically verify (or else report otherwise) that (1) the
precondition is strong enough to guarantee the absence of runtime errors in the subprogram, and (2) every call satisfies theprecondition. In order to gain DO-178C / ED-12C credit,
CodePeer needs to be qualified at level TQL-5 for thecorresponding activity. Analogously for the SPARK tools, for codethat adheres to the SPARK language subset.

Frédéric Pothon & Quentin Ochem

The methods and activities adopted to address the robustness issue should
be described in the software plans and, when applicable, in the softwaredevelopment standards (requirements and/or code standards).
Note that pre- or postcondition contracts do not in themselves implement
robustness requirements. Instead they help to formalize and verify suchrequirements (through static analysis, formal proof, or testing). The
robustness code is the code that is developed, if any, to make sure thatthese contracts are respected.

4.2.5.
Defining and Verifying a Code Standard
with GNATcheck and GNAT2XML
Contributions
Objectives

Software Planning Process (A-1[5]: 4.1.e)
Software Coding (A-2[6]: 5.3.1.a)
Reviews and Analyses of Source Code (A-5[4]: 6.3.4.d)

Activities

Software Planning Process Activities (4.2.b)
Software Development Standards (4.5.b, 4.5.c)
Software Coding (5.3.2.b)
Reviews and Analyses of Source Code (6.3.4)

Defining a Software Code Standard serves at least two purposes:

It helps to make the application source code consistent, moreverifiable, and more easily maintainable. While these qualities
do not have a direct safety benefit, adherence to a code
standard will improve the efficiency of the source code
verification activities.



It can prevent the use of language features that complicate
software product verification or introduce potential safety issues.
A common example is the deallocation of dynamically allocatedobjects, which can lead to dangling references if used incorrectly.
Verification that a program is not susceptible to such errors would

67

AdaCore Technologies for DO-178C / ED-12C

require thorough and complex analysis, and as a result it’s typicalfor a code standard to prohibit deallocation.
GNATcheck provides an extensive set of user-selectable rules to verify
compliance with various Ada coding standard requirements. These
includes style convention enforcement (casing, indentation, etc.), detectionof features that are susceptible to misuse (floating-point equality, goto
statements), static complexity checks (block nesting, cyclomatic complexity)and detection of features with complex run-time semantics (tasking,dynamic memory).
Since a code standard may include qualitative rules, or rules that are nothandled by GNATcheck, verifying that the source code complies with thestandard is not always fully automatable. However, there are two ways
to extend automated verification:

GNATcheck’s rules are extended on a regular basis in response
to customer input, and the tool’s enforcement of the new rules iseligible for qualification. Even in the absence of tool qualification,
the tool can still save time during verification by detecting ruleviolations.



Users can define their own rules as well, in particular using the
GNAT2XML tool. GNAT2XML transforms an Ada syntax tree into
an XML file, making it very easy for a third party to develop achecker based on XML technologies such as XPath.

One issue that comes up with a code standard is how to apply it
retrospectively to an existing code base. The first time a compliancechecking tool is run, it would not be uncommon to find hundreds or eventhousands of deviations. Fixing them all is not only a cumbersome andtedious task, but as a manual activity it’s also a potential for introducing
new errors into the code. As a result, it is often more practical to focus on
those deviations that are directly linked to safety, rather than trying to
update the entire application. Then for newly written code the compliancechecker can verify that no new deviations are introduced. Deviation
identification may be monitored (e.g. with SonarQube or SQUORE) andviewed with AdaCore’s GNATdashboard tool. This approach can provide
an analysis over time, for example showing the progress of removal ofcertain categories of deviations that were present in a given baseline.
68

Frédéric Pothon & Quentin Ochem

Another practicality with code standards is that some rules might need toadmit deviations in specific contexts when justified (for example the goto
statement might be acceptable to implement state transitions in code thatsimulates a finite-state machine, and be forbidden elsewhere).
GNATcheck allows adding local check exemptions, around a statement ora piece of code. Such exemptions and their justification would thenappear in the tool’s report.
TQL-5 qualification material is available for GNATcheck.

4.2.6.
Checking source code accuracy andconsistency with CodePeer
Contributions
Objectives

Reviews and Analyses of Source Code (A-5[6]: 6.3.4.f)

Activities

Reviews and Analyses of Source Code (6.3.4)“Accuracy and consistency” is a rather broad objective in DO-178C / ED12C, identifying a range of development errors that need to beprevented. Satisfying this objective requires a combination of reviews,
analyses and tests, and tools may be used for some of these activities.
CodePeer specifically targets issues that correspond to Ada exceptions,such as scalar overflow, range constraint violations, and array indexing
errors. It also detects other errors including reads of uninitialized
variables, useless assignments, and data corruption due to race conditions.
CodePeer handles all versions of the Ada language standard, from Ada
83 through Ada 2012, without any restrictions or additional annotation.
Since CodePeer’s conservative analysis may flag constructs that in fact
are correct, the tool’s output report needs to be manually reviewed sothat such “false alarms” can be discarded. This issue is common to allsound static analysis tools; i.e., if a tool detects all instances of a given
potential error, then it will sometimes diagnose correct code as containing
an error.
TQL-5 qualification material is available for CodePeer.

69

AdaCore Technologies for DO-178C / ED-12C

4.2.7.
Checking worst case stackconsumption with GNATstack
Contributions
Objectives

Reviews and Analyses of Source Code (A-5[6]: 6.3.4.f)

Activities

Reviews and Analyses of Source Code (6.3.4)

Stack usage is one of the items listed in the “source code accuracy andconsistency” objective; i.e., ensuring that the application has sufficient
stack memory reserved during program execution. Verification is often
achieved by running test cases and measuring the actual stack space
used. This approach may provide a false sense of confidence, however,since there is no evidence that the worst case usage has been addressed.
A more precise analysis method is to statically determine the actual stackconsumption, looking at the memory statically allocated by the compiler
together with the stack usage implied by the subprogram call graphs. The
GNATstack tool can perform this analysis for Ada and C, determining the
maximum amount of memory needed for each task stack.
In many cases, however, not everything can be statically computed;
examples are recursive calls, dynamically sized stack frames, and system
calls. In such cases, the user can provide a worst-case estimate as input to
GNATstack’s computation.
TQL-5 qualification material is available for GNATstack.

70

Frédéric Pothon & Quentin Ochem

4.2.8.

Compiling with the GNAT Pro compiler
Contributions

Objectives

Integration Process (A-2[7]: 5.4.1.a)
Reviews and Analyses of Integration (A-5[7]: 6.3.5.a)

Activities

Integration Process (5.4.2.a, 5.4.2.b, 5.4.2.d)
Reviews and Analyses of Integration (6.3.5)
Software Development Environment (4.4.1.f)

GNAT Pro is a gcc-based Ada and C compilation toolsuite that is widelyused by developers of high assurance software, in particular in a DO178C / ED-12C context. It is available on a broad range of platforms,
both native and cross. Embedded targets include various RTOSes forcertified applications (such as VxWorks 653, VxWorks 6 Cert, Lynx178,
PikeOS) as well as bare metal configurations, for a wide range ofprocessors (such as PowerPC and ARM).
The Ada language helps reduce the risk of introducing errors duringsoftware development (see [7]). This is achieved through a combination of
specific programming constructs together with static and dynamic checks.
As a result, Ada code standards tend to be shorter and simpler than C
code standards, since many issues are taken care of by default. The
GNAT Pro compiler and linker provide detailed error and warning
diagnostics, making it easy to correct potential problems early in thedevelopment process.
As with all AdaCore tools, the list of known problems in the compiler is
kept up to date and is available to all subscribers to the technology. A
safety analysis of the list entries is also available, helping developers
assess potential impact and decide on appropriate actions. Possible
actions are code workarounds or a choice of a different set of compiler
code generation options.
For certain Ada language features the GNAT Pro compiler may generate
object code that is not directly traceable to source code. This nontraceable code can be verified using a traceability analysis as describedin Section 4.2.13.

71

AdaCore Technologies for DO-178C / ED-12C

4.2.9.

Using GNATtest for low-level testing
Contributions

Objectives

Software Testing (A-6[3,4]: 6.4.c, 6.4.d)
Review and Analyses of Test procedures (A-7[1]: 6.4.5.b)and results (A-7[2]: 6.4.5.c)

Activities

Normal Range Test Cases (6.4.2.1)
Robustness Test Cases (6.4.2.2)
Review and Analyses of Test procedures and results (6.4.5)
Software Verification Process Traceability (6.5.b, 6.5.c)

The software architecture is developed during the design process,identifying components and sometimes subcomponents. The behavior ofeach terminal component is defined through a set of low-level
requirements. Typically, low-level testing consists in
1. Developing test cases from the low-level requirements,
2. Implementing the test cases into test procedures,
3. Exercising the test procedures separately on one or morecomponents, and
4. Verifying the test results
GNATtest may be used to develop the test data. Test cases andprocedures are produced in the Ada language. The general approach isfor GNATtest to generate an Ada test harness around the component
under test, leaving the tester to complete test skeletons based on thepredefined test cases, with actual inputs and expected results. Since thetest generation in carried out in a systematic way, it’s very easy toidentify where tests are missing (they will be reported as nonimplemented).
The tool works iteratively. If it’s called a second time on a set of files thathave changed, it will identify the changes automatically, preserving
existing tests and generating new tests for newly added subprograms.

72

Frédéric Pothon & Quentin Ochem

A component under test may call external components. One possible
approach is to integrate the components incrementally. This has thebenefit of preserving the actual calls, but it may be difficult to accurately
manage the component interfaces. Another approach is to replace someof the called subprograms with dummy versions (stubs). GNATtest support
both approaches, and can generate stub skeletons if needed.
The functionality just described is common to most test tools. A novel anduseful feature of GNATtest is its ability to develop the test cases during
the design process. (Note that independence between design and test
cases is not required. Independence is required between codedevelopment and test case derivation, to satisfy the independence criteriaof objectives A6-3 and 4 for software level A and B).
Approach 1: Test cases are not specified in Ada specifications
A traditional approach can be followed by GNATtest – that is to say,tests cases are described outside of the Ada specification, but linked to aparticular function. When working this way, GNATtest will generate one
test per subprogram; for example :function Sqrt (X : Float) return Float;

This will generate one unique test procedure skeleton.
Approach 2: Test cases are developed during the design process
In this approach, Ada package specifications are considered as an outputof the design process (see Section 4.2.2). More than one test per
subprogram may be developed. Here’s a simple example:

73

AdaCore Technologies for DO-178C / ED-12C

function Sqrt (X : Float) return Float
with Pre=> X >= 0.0,
Post=> Sqrt'Result >= 0.0,
Test_Case =>(Name=> "test case 1",
Mode=> Nominal,
Requires => X = 16.0,
Ensures => Sqrt'Result = 4.0),
Test_Case =>(Name=> "test case 2",
Mode=> Robustness,
Requires => X < 0.0,
Ensures => raise Constraint_Errorwith "Non-negative value needed");As part of the specification for the Sqrt function, the GNAT-specificaspect Test_Case is used to define two test cases. The one named “testcase 1” is identified as Nominal, which means that the argument supplied
as Requires should satisfy the function’s precondition, and the argument
supplied as Ensures should satisfy the function’s postcondition. The test
case named “test case 2” is specified as Robustness, so the pre- andpostconditions are ignored. As with all test cases, these are based on thefunction’s requirements.
When generating the test harness, GNATtest provides a skeleton of thetest procedures, and the user has to plug in the input values (from theRequires argument) and the expected results (from the Ensuresargument) for all test cases defined in the Ada package specification.
GNATtest will insert specific checks to verify that, within “test case 1”, allcalls made to Sqrt have X equal to 16.0, and each value returned isequal to 4.0. This not only verifies that the test succeeded, but also
confirms that the test conducted is indeed the intended test. As a result,
GNATtest verifies that the test procedures comply with the test cases, thatthey are complete (all test cases have been implemented and exercised),
and that the test results are as expected.
In addition, the traceability between test case, test procedures and test
results is direct, and does not require production of further trace data.

74

Frédéric Pothon & Quentin Ochem

Approach 3: Test case are developed separately from the design
process
The two test cases developed in Approach 2 are not sufficient to fully
verify the Sqrt function. To comply with DO-178C / ED-12C Table A-6
Objectives 3 and 4, the activities presented in §6.4.2 (RequirementsBased Test Selection) for normal and robustness cases are applicable. It is
not generally practical to include all the test cases in the Ada package
specification.
Another consideration is the criterion of independence between code andtest case development. Thus Approach 2 is applicable only if the Ada
package specification is developed during the design process (and notduring the coding process).
An alternative approach is to develop the test data separately from theAda package specifications, while some “meta” test cases (or test case“classes”) are still defined and used by GNATtest to develop the test
harness. Here’s an example:
function Sqrt (X : Float) return Float
with Test_Case =>(Name=> "test case 1",
Mode=> Nominal,
Requires => X > 0.0,
Ensures => Sqrt'Result > 0.0),
Test_Case =>(Name=> "test case 2",
Mode=> Nominal,
Requires => X = 0.0,
Ensures => Sqrt'Result = 0.0),
Test_Case =>(Name=> "test case 3",
Mode=> Robustness,
Requires => X < 0.0,
Ensures => raise Constraint_Errorwith "Non-negative value needed");In this approach, three “meta” test cases are identified, defining the
expected high-level characteristics of the function. For each “meta” test
case, at least one actual test case will be developed. In this example, at

75

AdaCore Technologies for DO-178C / ED-12C

least three test cases need to be defined, corresponding to an actual
parameter that is positive, zero, or negative, with the respective
expected results of positive, zero, and raising an exception.
As in Approach 2, the skeleton generated by GNATtest must becompleted by the user, but in that case the data produced are the actual
test cases (and cannot be considered as test procedures). For example,
based on the range of the input, the user should define tests for boundary
values, for the value 1, or any representative data (equivalent classes).
As previously, GNATtest will insert specific checks for the 3 “meta” test
cases. Then GNATtest will verify that at least one test case for each“meta” test case has been implemented, and that the results are correct.
Note that in this approach, the test procedures become the internal files
generated by GNATtest. Therefore, as it will be difficult to verify thecorrectness of these files, GNATtest qualification is needed in order tosatisfy objective A7-1 “test procedures are correct”.

4.2.10.
Using GNATemulator for low-level andsoftware / software integration tests
Contributions
Objectives

Software testing (A-6[1,2,3,4]: 6.4.a, 6.4.b, 6.4.c, 6.4.d)

Activities

Test environment (6.4.1)
Software Integration testing (6.4.3.b)
Low Level testing (6.4.3.c)
Structural coverage analysis (6.4.4.2.a)

As stated in DO-178C/ED-12C §6.4.1:“More than one test environment may be needed to satisfy theobjectives for software testing.... Certification credit may be
given for testing done using a target computer emulator or a hostcomputer simulator”.
But an integrated target computer environment is still necessary to satisfy
the verification objective (A6-5) that the executable object code is76

Frédéric Pothon & Quentin Ochem

compatible with the target computer. These tests, referred to as“Hardware / Software integration tests”, are necessary since some errors
might only be detected in this environment. As stated in DO-330 / ED215, FAQ D.3, qualification of a target emulator or simulator may berequired if they are used to execute the Hardware / Software
integration tests.
Although GNATemulator might thus not be applicable in the scope ofHardware / Software integration tests, it is allowed for all other tests(see DO-330 / ED-215 FAQ D.3). Two approaches may be used:To perform some tests (that may be part of low-level testing
and/or Software / Software integration testing) on
GNATemulator, and to claim credit on this environment forsatisfying the objectives concerning the Executable Object Code’s
compliance with its requirements

To use GNATemulator to prototype and gain confidence in tests
prior to re-running the tests on the actual target computer
environment.

In any event GNATemulator helps considerably in the early detection oferrors in both the software and the test procedures. GNATemulator works
in much the same fashion as a “Just In Time” (JIT) compiler: it analyzes thetarget instructions as it encounters them and translates them on the fly (ifnot done previously) into host instructions, for example an x86. This makes
it particularly suitable for low-level testing, at least for those tests that do
not depend on actual timing on the target.
GNATemulator also provides an easy way to interact with emulated
devices and drivers on the host. Reads and writes to emulated memory
can trigger interactions with such code, through the GNATbus interface.
GNATemulator can be used with the GNATcoverage tool for structural
coverage analysis. As long as the test environment with GNATemulator is
acceptable for analyzing the structural coverage, there is no need toexercise the tests twice (as is typically done when the analysis isperformed on instrumented code).

77

AdaCore Technologies for DO-178C / ED-12C

4.2.11.
Structural code coverage with
GNATcoverageContributions
Objectives

Test Coverage Analysis (A-7[5]: 6.4.4.c)

Activities

Structural Coverage Analysis (6.4.4.2.a, 6.4.4.2.b)

The structural coverage analysis objectives of DO-178C / ED-12C serve
to verify the thoroughness of the requirements-based tests and to help
detect unintended functionality. The scope of this analysis depends on theDevelopment Assurance Level:Statement coverage for Level C,Statement and Decision coverage for level B, and

Statement, Decision and Modified Condition / Decision Coverage(MC/DC) at level A.

These three criteria will be explained through a simple (and artificial)
example, to determine whether a command should be issued to open theaircraft doors:
Closed_Doors: Integer;
Open_Ordered, Plane_Landed : Boolean;...
if Closed_Doors > 0 and then Open_Ordered and thenPlane_Landed then
Open_Doors;
end if;

Note: the Ada short-circuit form “and then” is equivalent to the C shortcut
boolean operator “&&”.
This code fragment consists of two statements:


78

The enclosing “if” statement

Frédéric Pothon & Quentin OchemThe enclosed “Open_Doors;” statement, which will be executed if
the decision in the “if” statement is True

The “if” statement in turn contains a single decision:
Closed_Doors > 0 and then Open_Ordered and then Plane_Landed

and this decision contains three conditions:

Close_Doors > 0Open_Ordered

Plane_Landed

At the statement level, both statements need to be executed during
requirements-based tests. This criterion may be achieved with only one
test, with all three conditions True.
It’s important to realize that this piece of code is the implementation of
one or several requirements, and a single test with all three conditions
True will almost certainly fail to satisfy the requirement coverage
criterion. Further, this single test is probably not sufficient to detect
implementation errors: the purpose of testing is to detect errors, not toachieve structural code coverage. Structural coverage analysis is mainly atest completeness activity.
At the decision level, each decision must be exercised both with a Trueand False outcome. In the example above, this may be achieved with only
two tests; one test with all three conditions True, and a second test with atleast one False.
The third level is called MC/DC, for Modified Condition / Decision
Coverage. The goal is to assess that each condition within a decision has
an impact, independently of other conditions, on the decision outcome.
The motivation for MC/DC is most easily appreciated if we first look atwhat would be required for full coverage of each possible combination oftruth values for the constituent conditions. This would require eight tests,
represented in the following table:

79

AdaCore Technologies for DO-178C / ED-12C

Closed_Doors > 0

Open_Ordered

Plane_Landed

Result

True

True

True

True

True

True

False

False

True

False

True

False

True

False

False

False

False

True

True

False

False

True

False

False

False

False

True

False

False

False

False

False

In the general case, 2n cases would be needed for a decision with n
conditions, and this would be impractical for all but small values of n. The
MC/DC criterion is achieved by selecting combinations demonstrating thateach condition contributes to the outcome of the decision.
With MC/DC, each condition in the decision must be exercised with both
True and False values, and each condition must be shown to
independently affect the result. That is, each condition must be exercisedby two tests, one with that condition True and the other with the condition
False, such that:

The result of the decision is different in the two tests, andFor each other condition, the condition is either True in both tests
or False in both tests

Here the MC/DC criteria may be achieved with four tests: one test withall three conditions True, and each other test changing the value of one
condition to False:
Closed_Doors>0

Open_Ordered

Plane_Landed

ResultBaseline

True

True

True

True

Test 1

False

True

True

False

Test 2

True

False

True

False

Test 3

True

True

False

False

80

Frédéric Pothon & Quentin Ochem

Each condition thus has two associated tests, the one marked as baseline,
and the one with an italicized False in that condition’s column. These two
tests show how that condition independently affects the outcome: The
given condition is True in the baseline and False in the other, each othercondition has the same value in both tests, and the outcome of the two
tests is different.
In the general case, the MC/DC criterion for a decision with n conditions
requires n+1 tests, instead of 2n. For more information about MC/DC, see[10].
GNATcoverage handles all three levels of structural code coverage. It
reports this both for Ada and C source code. Moreover, the
GNATcoverage technology does not require source code instrumentation.
Most code coverage technologies instrument the code (either at source orobject level) to insert logging commands between statements anddecisions to track execution. This requires performing the test twice, one
execution for verification of compliance with the requirements, and asecond (with instrumented code) for structural coverage analysis.
GNATcoverage is based on the instrumentation of the execution platform,
so there is no modification of the code being tested. GNATcoverage canoperate with several execution environments:
On an emulation platform (e.g. GNATemulator) that can generatea binary execution trace,On a native platforms with a virtualization layer (such as
Valgrind or DynamoRIO) that can generate a binary execution
traces, orOn actual hardware with a probe supporting real-time tracing(such as a Nexus interface) that can retrieve binary execution
information.

Selection of one of these approaches is based on hardware constraints
and on test environment capabilities. For example, hardware may or may
not have real-time tracing available.
Although the coverage data generated by an execution trace is in termsof the object code (instruction or branch coverage), this is not sufficient to81

AdaCore Technologies for DO-178C / ED-12C

determine whether MC/DC has been achieved. GNATcoverage handles
this issue by using static information generated by the compiler (either for
Ada or for C) that conveys the relationship between the source code andthe binary.
TQL-5 qualification material is available for GNATcoverage.

4.2.12.
Data and control coupling coveragewith GNATcoverageContributions
Objectives

Test Coverage Analysis (A-7[8]: 6.4.4.d)

Activities

Structural Coverage Analysis (6.4.4.2.c)

DO-178C / ED-12C objective A7-8 states:“Test coverage of software structure (data coupling and control
coupling) is achieved”.
This is part of overall structural coverage analysis. Although structural
coverage activities (statement, decision, or MC/DC) can be carried out atvarious times, it is often performed during low-level testing. This allows
precise control and monitoring of test inputs and code execution. If code
coverage data is retrieved during low-level testing, structural coverage
analysis can assess the completeness of the low-level tests.
In addition, the completeness of the integration tests needs to be verified.
For that purpose the integration tests have to be shown to exercise theinteractions between components that are otherwise tested independently.
This is done through data and control coupling coverage activities. Eachdata and control coupling relationship must be exercised at least once
during integration tests.
Data and control coupling are the interfaces between components, as
defined in the architecture. More specifically, data coupling concerns thedata objects that are passed between modules. These may be global
variables, subprogram parameters, or any other data passing
mechanisms. Control coupling concerns the influence on control flow. Inter82

Frédéric Pothon & Quentin Ochem

module subprogram calls are obvious cases of control coupling (theyinitiate a control flow sequence) but subtler cases such as a global
variable influencing a condition can be also considered as control
coupling. For example, if module Alpha has something like:
if G then
Do_Something;else
Do_Something_Else;end if;and in a module Beta:
G := False;

Then this is really an example of control coupling, and not data coupling.
Using a global variable to effect this control flow is considered an
implementation choice.
In the software engineering literature, the term “coupling” generally has
negative connotations since high coupling can interfere with a module’s
maintainability and reusability. In DO-178C / ED-12C there is no suchnegative connotation; coupling simply indicates a relationship between
two modules. That relationship needs to be defined in the softwarearchitecture and verified by requirements-based integration tests.
One strategy to verify coverage of data and control coupling is toperform statement coverage analysis during integration testing.
GNATcoverage may be used in this way to detect incomplete executionof such data and control flows. This may require coding constraints, suchas limited use of global data, or additional verification for such data:Parameter passing and subprogram calls: Statement coverage
ensures that all subprograms are called at least onceGlobal data: Statement coverage ensures that all uses
(read/write) of global data are exercised at least once.

83

AdaCore Technologies for DO-178C / ED-12C

4.2.13.
Demonstrating traceability of source toobject code
Contributions
Objectives

Test Coverage Analysis (A-7[5]: 6.4.4.c)

Activities

Structural Coverage Analysis (6.4.4.2.b)

For DAL A software, DO-178C/ED-12C objective A7-9 requires
identifying if code not visible at the source code level is added by thecompiler, linker, or other means; if so, it is necessary to verify such codefor correctness. Compiler-added code typically takes the form of extra
branches or loops that are explicit in the object code but not at the source
level. One example in Ada is the implicit checking that is often requiredby the language semantics.
A statement like:A : Integer range 1..10;
B : Integer;...
A := B;

may be compiled into the following pseudo-object code:
if B >= 1 or else B <= 10 thenA := B;else
raise Constraint_Error;
end if;This assumes that checks are retained at run-time. However, even withchecks disabled, a compiler for either Ada or C may still need togenerate non-traceable code to implement some language constructs. An
Ada example is array slice assignment, which results in loops at the object
code level on typical target hardware:

84

Frédéric Pothon & Quentin Ochem

A, B : String (1..100)...
A (1..50) := B (11..60);

AdaCore has verified the correctness of non-traceable code for GNAT
Pro Ada and GNAT Pro C, based on representative samples of sourcecode. Samples were chosen for the language features permitted bycommon code standards. Object code was generated for each sample,
and any additional (non-traceable) code was identified. For each nontraceable feature, additional requirements and tests were provided toverify that the behavior of the resulting code was indeed as required.
Traceability analyses for GNAT Pro Ada and GNAT Pro C are available.
These analyses take into account the specific compiler version, compiler
options, and code standard that are used, to ensure that the code
samples chosen are representative. If some specific language features,
options, or compiler versions are not suitable for the analysis, appropriate
adaptations are made.

85

AdaCore Technologies for DO-178C / ED-12C

4.3. Use case #1b: Coding with Ada using OOT
featuresThis use case is based on use case #1, taking advantage of Ada and the
AdaCore ecosystem, but with a design that uses Object-Oriented
Technologies. As a result, the following “vulnerabilities” identified in thetechnology supplement DO-332 / ED-217 need to be addressed:


Local type consistencyDynamic memory management

Parametric polymorphism (genericity)OverloadingType conversion



Exception management

Component-based development

4.3.1.

Object orientation for the architecture
Contributions

Objectives

Software Design Process Objectives (A-2[4]: 5.2.1.a)

Activities

Software Design Process Activities (OO.5.2.2.h)
Software Development Process Traceability (OO.5.5.d)

Vulnerabilities

Traceability (OO.D.2.1)

Object orientation is a design methodology, a way to compose a system
where the focus is on the kinds of entities that the system deals with, andtheir interrelationships. Choosing an object-oriented design will thus havea significant impact on the architecture, which is expressed in terms ofclasses and their methods (or primitive operations in Ada). Thisarchitecture can be modeled in many ways, for example with UML class
diagrams.

86

Frédéric Pothon & Quentin Ochem

The use of OOT can affect traceability between low-level requirements
and code. Without object orientation, traceability is generally between a
set of requirements and one module, one function or one piece of code. Inan object-oriented design, as defined in DO-332 / ED-217, §O.O.5.5:“All functionality is implemented in methods; therefore,
traceability is from requirements to the methods and attributes
that implement the requirements”.

4.3.2.

Coverage in the case of generics
Contributions

Objectives

Test Coverage Analysis (A-7[4,5]: 6.4.4.b, 6.4.4.c)

Activities

Requirement coverage analysis (6.4.4.1)
Structural Coverage Analysis (6.4.4.2.a, 6.4.4.2.b)

Vulnerabilities

Parametric Polymorphism (OO.D.1.2)
Structural Coverage (OO.D.2.2)

Genericity is one of the “related techniques” (not part of OOT) that iscovered by DO-332 / ED-217. A generic unit is a template for a pieceof code that can be instantiated with different parameters, including
types and subprograms. A complication with respect to certification is thatthe same generic unit may have different instantiations that behave
differently. Consider, for example, a simple generic Ada function that canbe instantiated with an integer type to perform some basic computation:
generic
type Int_Type is range <>;function Add_Saturated (Left, Right, Max : Int_Type) return
Int_Typewith Pre => Max>0;87

AdaCore Technologies for DO-178C / ED-12C

function Add_Saturated (Left, Right, Max : Int_Type) return
Int_Type isTemp : Int_Type;
begin
Temp := Left + Right;
if Temp > Max thenreturn Max;elsif Temp < -Max thenreturn -Max;
else
return Temp;
end if;end Add_Saturated;

Then consider two separate instantiations:with Add_Saturated;
procedure Test_Gen isfunction Add_1 is new Add_Saturated (Integer);
type Small_Int is range -10 .. 10;
function Add_2 is new Add_Saturated (Small_Int);
N1 : Integer;
N2 : Small_Int;
begin
N1 := Add_1 (6, 6, 10); -- Correctly yields 10
N2 := Add_2 (6, 6, 10); -- Raises Constraint_Error
end Test_Gen;

Calling Add_1 (6, 6, 10) will yield 10 as a result. Calling Add_2 (6,6, 10) will raise Constraint_Error on the first addition, since the sum
Left+Right will be equal to 12 and therefore violate the range
constraint for Small_Int.
Different instantiations of the same generic unit can thus exhibit different
behaviors. As a result, DO-332 / ED-217 specifies that each genericinstance must be tested (and covered).

88

Frédéric Pothon & Quentin Ochem

GNATtest will generate a test harness taking this requirement into
account. In particular, it will generate a separate testing setup for each
instance, while keeping a generic test procedure for all of them.
GNATcoverage can separately report the coverage of each genericinstance, based on the “-S instance” switch.
With respect to traceability, the code of a generic instantiation istraceable to the source. Indeed, at the point of instantiation, the effect isas though the generic template were expanded in place, with formal
parameters replaced by the actuals. (This expansion is not at the level ofsource text, but rather is based on a program representation where allnames have been semantically resolved.) As a result, using a genericdoesn’t add any non-traceable code. Code is traced from the generic
template to the object code, once per instance.

4.3.3.
Dealing with dynamic dispatching andsubstitutability
Contributions
Objectives

Software Design Process Objectives (A-2[4]: 5.2.1.a)
Local Type Consistency Verification Objective (OO.A7[OO 10]: OO.6.7.1)

Activities

Software Design Process Activities (OO.5.2.2.i)
Local Type Consistency Verification Activity (OO.6.7.2)

Vulnerabilities

Inheritance (OO.D.1.1)

One of the major features of OOT is dynamic dispatching (also called“dynamic binding”), which adds considerable expressive power but alsopresents challenges to verification. With dynamic dispatching, thesubprogram to be invoked on a reference to a target object is not known
statically but rather is resolved at run time based on which class thetarget object belongs to. This differs from a call through an access-tosubprogram value in the sense that, with dynamic dispatching, thepotential destination subprograms are constrained to a specific classhierarchy as determined by the type of the reference to the target object(the “controlling parameter”, in Ada terms).

89

AdaCore Technologies for DO-178C / ED-12C

In Ada, a subprogram that can be invoked through dynamic dispatching –this is known as a “primitive subprogram” – can never be removed by a
subclass; it is either inherited or overridden. Thus on a call that isdynamically dispatched, although it is not known at compile time whichsubclass’s version of the subprogram will be invoked, some subclass’s
implementation of the subprogram will indeed be called. Ada is not
susceptible to “no such method” errors that can arise with dynamic
dispatching in some other languages.
Understanding Substitutability
From a safety point of view, not knowing the specific target of a given
call introduces significant issues for verifiability. DO-332 / ED-217 statesthat if an inheritance hierarchy is constructed so that each subclassspecializes its superclass (i.e., wherever a superclass instance is permitted
a subclass instance may be substituted) then dynamic dispatching is
acceptable. This substitutability property for a class inheritance hierarchy
is known as the “Liskov Substitution Principle” (LSP).
If a hierarchy complies with LSP, then testing and other verification can be
conducted based on properties defined at the class level, which will thenneed to be respected by each subclass. As we shall see, this has
implications on the pre- and postconditions that are allowed when adispatching subprogram is overridden.
Here is a specific – although simplified – example: an aircraft type with asubprogram that is supposed to open the doors.
package Aircraft_Pkg istype Aircraft is abstract tagged private;procedure Open_Doors (Self : Aircraft)with Pre'Class => Self.On_Ground,
Post'Class => Self.Doors_Opened;...
private...
end Aircraft_Pkg;

90

Frédéric Pothon & Quentin Ochem

The contracts for the pre- and postconditions reflect the low-level
requirements:the aircraft has to be on the ground prior to having its doors
opened, andthe doors are opened as a result of the call.

The Aircraft type could be used as follows:
procedure Landing_Procedure (My_Aircraft : Aircraft'Class) is
begin
...
while not My_Aircraft.On_Ground loop...
end loop;-- Here if My_Aircraft is on the ground
My_Aircraft.Open_Doors; -- Dispatching call
My_Aircraft.Let_Passengers_Out;...
end Landing_Procedure;

We’re first waiting until the aircraft is actually on the ground, then open
the doors, then as the doors are opened we let passengers out.
All types in the Aircraft inheritance hierarchy have to comply with theAircraft contracts. That is, for any type in the Aircraft'Class hierarchy,
the Open_Doors subprogram for that type can require at most theOn_Ground precondition and nothing stronger. If a stronger precondition
were imposed, then a dynamically dispatching call of Open_Doors could
fail if the actual parameter were of this (non-substitutable) type. The
extra precondition would not necessarily be known to clients of the root
type Aircraft.
Analogously for the postcondition, any type in the Aircraft'Classhierarchy has to guarantee at least the Doors_Opened property, since
this will be assumed by callers of Open_Doors.
In short, the substitutability property can be summarized as follows:91

AdaCore Technologies for DO-178C / ED-12C

If a type hierarchy is to be substitutable, then a dispatching
subprogram for a derived type can weaken but not strengthen
the precondition of the overridden subprogram for its parent
type, and can strengthen but not weaken the postcondition.
The class-wide Pre'Class and Post'Class aspects are inherited (unlessoverridden) and have other semantics that directly support thissubstitutability property. The specific (non-class-wide) aspects Pre andPost are not inherited and should only be used if the hierarchy does notsupport substitutability.
Let’s now define a Jet:
type Jet is new Aircraft with ...
overriding
procedure Open_Doors (Self : Jet)
with Pre=> Self.On_Ground and Self.Engines_Off,
Post'Class => Self.Doors_Opened and not Self.Pressurized;

Suppose that Landing_Procedure is invoked on an object of type Jet:
J : Aircraft'Class := Jet'(...);...
Landing_Procedure (J);In the call My_Aircraft.Open_Doors, first the precondition for
Open_Doors for Aircraft will be evaluated (since the actual parameter
is of the class-wide type Aircraft'Class. That’s not a problem, since thecaller sees this precondition. However, then the specific precondition for
Open_Doors for Jet is evaluated, and there is a problem with theadditional constraint – requiring the engines to be off. The Jet type
could have been defined long after the Landing_Procedure
subprogram was written, so the design of the Landing_Procedure code
would not have taken the added precondition into account. As a result,the Open_Doors procedure could be invoked when the engines were stillrunning, violating the requirement. (With run-time assertion checking
enabled, an exception would be raised.) The type Jet is not substitutable
for the type Aircraft on invocations of Open_Doors.

92

Frédéric Pothon & Quentin Ochem

The non-substitutabiity is reflected in the use of the specific aspect Pre
rather than the class-wide aspect Pre'Class. In a type hierarchy rooted
at type T where Pre'Class is specified at each level for a subprogram
Proc, the effective precondition for a dispatching call X.Proc where X isof the type T'Class is simply the precondition specified for Proc for theroot type T (which is the only precondition known to the caller). In the Jet
example, if Pre'Class had been used, a dispatching call to Open_Doors
would not check the Engines_Off condition.
In short, if a subclass is to be substitutable then it may weaken but notstrengthen a subprogram’s precondition, and it should use Pre'Class
rather than Pre. If a subclass needs to strengthen a precondition then it is
not substitutable and should use Pre rather than Pre'Class.
The postcondition for Open_Doors for Jet does not have this problem. It
adds an additional guarantee: pressurization is off after the opening of
the doors. That’s OK; it doesn’t contradict the expectations of theLanding_Procedure subprogram, it just adds an additional guarantee.
The Jet type illustrated non-substitutability due to precondition
strengthening. Non-substitutability can also arise for postconditions, as
illustrated in a slight variation of the Aircraft type:package Aircraft_Pkg istype Aircraft is abstract tagged private;procedure Open_Doors (Self : Aircraft)with Pre'Class => Self.On_Ground,
Post=> Self.Doors_Opened; -- Specific, notclass-wide...
private...
end Aircraft_Pkg;

Here’s a possible declaration for a hot air balloon:

93

AdaCore Technologies for DO-178C / ED-12C

type Hot_Air_Balloon is new Aircraft with ...
overriding
procedure Open_Doors (Self : Hot_Air_Balloon)with Pre'Class => Self.On_Ground or Self.Tethered,
Post=> Self.Doors_Unlocked;

In this case, the precondition is relaxed (we’re assuming a short tether).
This is acceptable, since the landing procedure will still check the stronger
precondition and wait for the aircraft to be on the ground; the class-wide
precondition of the root type is checked on a dispatching call. (Theweaker precondition would be checked on a call such as B.Open_Doors
where B is either of the specific type Hot_Air_Balloon or the classwide type Hot_Air_Balloon'Class.)
However, a Hot_Air_Balloon is less automated than a Jet: the doors
don’t open automatically, they just unlock. The Landing_Procedure
subprogram assumes the postcondition for Aircraft (that the doors are
opened), but this is not guaranteed for a Hot_Air_Balloon, so
passengers might be pushed out while the doors are unlocked but stillclosed. The new postcondition is breaking the requirement by weakening
its parent type’s postcondition, and this is not acceptable. Thus the
Hot_Air_Balloon type is not substitutable for Aircraft.
Substitutability defects may be evidence of a number of problems; forexample, the hierarchy of classes or requirements may be incorrect, or theclasses may be modeling properties inappropriately. Overall, thisindicates design issues to be addressed when specifying the low-level
requirements and/or architecture.
A natural question is how to detect substitutability defects (or achieve
confidence that such defects are not present) in the application. DO-332/ ED-217 provides three approaches: pessimistic testing, local substitution
tests, or formal proofs.
Verifying substitutability by pessimistic testing
Pessimistic testing is conceptually the easiest to understand. The idea is totest at each point of dispatch all possible types that could be substituted.
In the Landing_Procedure example, assuming that our system is94

Frédéric Pothon & Quentin Ochem

managing both jets and hot air balloons, this would mean two sets oftests: one for the Jet type, and one for Hot_Air_Balloon. This is working
around the difficulty of not knowing statically the potential target of acall: we just test all possible scenarios.
This is particularly appropriate with “flat” hierarchies, which may bebroad but not deep. An example is an OOP design pattern for an
abstract root type (such as a container data structure) with concrete
specializations corresponding to different representational choices. In thiscase, regular requirement-based testing is equivalent to pessimistic
testing. However, the complexity of additional testing can quickly become
unmanageable as the depth of the class hierarchy increases.
Verifying substitutability through requirement-based testing
In this case verification of substitutability is done on top of regular testing.
In the above examples the Aircraft, Jet and Hot_Air_Balloon
requirements are all associated with specific requirement-based tests.
Substitutability can be demonstrated by running top level tests withinstances of other types of the class. In other words, tests developed
based on requirements of Aircraft must pass with instances of Jet and
Hot_Air_Balloon. This is enough to demonstrate substitutability,
effectively testing the substitution. This may require more or fewer tests
depending on OOP usage. In particular, for large class hierarchies,
testing at the class level is much more cost-effective than testing every
possible target of every possible dispatching call in the actual code.
The GNATtest tool supports generation of the appropriate test
framework for substitution testing; see the GNATtest option --validatetype-extensions .
Verifying substitutability through formal proof
In conjunction with DO-333 / ED-216 (Formal Methods supplement), andassuming that requirements can be expressed in the form of pre- andpostconditions, the consistency between an overriding subprogram and its
parent type’s version can be verified through formal proof. This can bedone in particular with the SPARK language. There are two criteria for
substitutability:95

AdaCore Technologies for DO-178C / ED-12C

The precondition of a subprogram for a type must imply theprecondition of each overriding subprogram in the classhierarchy.

The postcondition of any overriding subprogram for a type must
imply the postcondition of the corresponding subprogram foreach ancestor type in the hierarchy

These preconditions and postconditions – or requirements – must also beverified, through either requirement-based testing or formal proofs.
The SPARK tool can verify consistency of classes of types, and inparticular consistency of pre- and postconditions as described above. To
enable such verification, these must be declared as class-wide contracts
as in the initial example of the Aircraft type above.
Differences between local and global substitutability
DO-332 / ED-217 does not require classes to be globally substitutable,
but only locally; that is, only around actual dispatching points. For
example, the following code is not globally substitutable, but is locally
substitutable at the dispatching calls:
package Aircraft_Pkg istype Aircraft is abstract tagged private;procedure Open_Doors (Self : Aircraft)with Pre'Class => Self.On_Ground,
Post'Class => Self.Doors_Opened;
procedure Take_Off (Self : Aircraft)with Pre'Class => Self.On_Ground and not
Self.Doors_Opened,
Post'Class => not Self.On_Ground;...
private...
end Aircraft_Pkg;

96

Frédéric Pothon & Quentin Ochem

package Aircraft_Pkg.Jet_Pkg istype Jet is new Aircraft with ...
overriding
procedure Open_Doors (Self : Jet)
with Pre=> Self.On_Ground and Self.Engines_Off,-- Not substitutable
Post'Class => not Self.Pressurized;
overriding
procedure Take_Off (Self : Aircraft)-- Inherit Aircraft's precondition
with Post'Class => not Self.On_Ground andSelf.Speed >= 100.0;...
private...
end Aircraft_Pkg.Jet_Pkg;...
X, Y : Aircraft'Class := Jet'(...)...
X.Take_Off;
Y.Take_Off;The Jet type is not globally substitutable for Aircraft, since theprecondition on Open_Doors for Jet is stronger than the precondition on
Open_Doors for Aircraft. But Jet is locally substitutable in the above
fragment:

The invocations X.Take_Off and Y.Take_Off dispatch to Jet,
but Jet is substitutable for Aircraft here:o

The precondition for Take_Off(Aircraft) is inheritedby Jet, ando

The postcondition for Take_Off(Aircraft) is
strengthened by Jet

97

AdaCore Technologies for DO-178C / ED-12C

Whether it is easier to demonstrate local versus global suitability for agiven class depends on the architecture and the ease of identification of
actual dispatch destinations and substitutability. DO-332 / ED-217 allows
the applicant to decide on whichever means is the most appropriate.

4.3.4.
Dispatching as a new module couplingmechanism
Contributions
Objectives

Test Coverage Analysis (A-7[8]: 6.4.4.d)

Activities

Structural Coverage Analysis (6.4.4.2.c)

Vulnerabilities

Structural Coverage (OO.D.2.2)

With procedural programming, modules can be interfaced, or coupled,through parameter passing, subprogram calls or global variables (dataand control coupling). Object orientation introduces a new way in which
two modules may interface with each other: by extension / typederivation. Following-up on previous examples:
procedure Control_Flight (Plane : Aircraft'Class) is
begin
...
-- Dispatching call, may call Take_Off from instances-- defined in other modules, creating coupling-- relationship with those modules
Plane.Take_Off;...
end Control_Flight;

Aircraft of different types may be defined in separate modules. A
connection between these modules and the rest of the application may bemade by dispatching from this call. All objectives that apply to control
and data coupling now apply to type derivation coupling, in particular98

Frédéric Pothon & Quentin Ochem

the coverage objectives. Whether or not testing with all possible
derivations in the system is used (i.e., pessimistic testing) depends of thestrategy chosen for substitutability demonstration.

4.3.5.

Memory management issues
Contributions

Objectives

Software Design Process Objectives (A-2[3,4]: 5.2.1.a)
Reviews and Analyses of Software Architecture (OO.A4[8]: OO.6.3.3.a)Dynamic Memory Management Verification Objective(OO.A-7[OO10]: OO.6.8.1)

Activities

Software Design Process Activities (OO.5.2.2.j)
Dynamic Memory Management Verification Activities(OO.6.8.2)
Reviews and Analyses of Software Architecture(OO.6.3.3)

Vulnerabilities

Dynamic Memory Management (OO.D.1.6)

In addition to local type consistency, which was described in thepreceding section, DO-332 / ED-217 also introduced another newverification objective: robustness of dynamic memory management. Thisobjective encompasses not only explicit use of dynamic memory, througheither automatic means (“garbage collection”) or application-provided
allocation / deallocation, but also implicit uses through higher level data
structures such as object collections of various kinds. DO-332 / ED-217
identifies a number of criteria that need to be met by any memory
management scheme:The allocator returns a reference to a valid piece of memory, nototherwise in use



If enough space is available, allocations will not fail due tomemory fragmentationAn allocation cannot fail because of insufficient reclamation of
inaccessible memory99

AdaCore Technologies for DO-178C / ED-12C

The total amount of memory needed by the application isavailable (that is, the application will not fail because of
insufficient memory)An object is only deallocated after it is no longer used

If the memory management system moves objects to avoid
fragmentation, inconsistent references are prevented



Allocations and deallocations complete in bounded time

Meeting these criteria may be the responsibility of the run-time memory
management library (referred to as the “memory management
infrastructure”, or MMI in DO-332 / ED-217) or the application code(AC). Table OO.D.1.6.3 in DO-332 / ED-217 presents several different
memory management techniques that can be used. For each technique thetable identifies whether the MMI or the AC is responsible for meeting
each criterion.
Dynamic memory is identified as a specific issue in object orientation
because, in many languages, it is very difficult or even impossible to use
object-oriented paradigms without dynamic memory management. This is
in particularly true for referenced-based languages such as Java.
Although dynamic memory is also helpful when OOP is used in Ada,
simple architectures may allow creating (and subsequently dispatching on)
stack-resident or library-level objects, without needing dynamic memory.
This can be done if such objects are of a class-wide type. The main
constraint is that each object has to be initialized at declaration, and its
specific type cannot change later. For example, the following codeprovides a function returning an object of a type in the Aircraft classhierarchy, depending on a parameter:
type Aircraft
is abstract tagged ...
type Jetis new Aircraft with ...
type Hot_Air_Balloon is new Aircraft with ...
...

100

Frédéric Pothon & Quentin Ochem

function Create (T : Integer) return Aircraft'Class is
begin
if T = 1 thenreturn Jet'(<initialization of a Jet>);elsif T = 2 thenreturn Hot_Air_Balloon'(…);-- initialization of a Hot_Air_Balloon
else
raise <some exception>;end if;end Create;

Objects of the class-wide type Aircraft'Class can be created as local
or global variables:
N : Integer:= Get_Integer;
P : Aircraft'Class := Create (N);...
P.Take_Off;-- Dynamically computed

Here, P is allocated on the stack and may be either a Jet or a
Hot_Air_Balloon. The call to P.Take_Off will dispatch accordingly.
For notational convenience it may be useful to reference objects of aclass-wide type through access values (pointers), since that makes it easier
to compose data structures, but to prevent dynamic allocation. This can beachieved in Ada:
type Aircraft
is abstract tagged ...
type Jetis new Aircraft with ...
type Hot_Air_Balloon is new Aircraft with ...
type Aircraft_Ref is access all Aircraft'Class;for Aircraft_Ref'Storage_Size use 0;-- No dynamic allocations
...

101

AdaCore Technologies for DO-178C / ED-12C

Jet_1, Jet_2: aliased Jet := ...;
Balloon_1, Balloon_2, Balloon_3 : aliased Hot_Air_Balloon :=...;type Aircraft_Pool_Type is array(Positive range <>) of
Aircraft_Ref;
Pool : Aircraft_Pool_Type := (Jet_2'Access,Balloon_3'Access,Jet_1'Access);...
for P of Pool loop
P.Take_Off; -- Dispatches
end loop;

These examples show how object orientation can be used in Ada without
dynamic memory. More complicated designs, however, would probably
need some form of dynamic memory and thus need to comply with thecriteria listed above.

4.3.6.

Exception handlingContributions

Objectives

Software Design Process Objectives (A-2[4]: 5.2.1.a)
Reviews and Analyses of Software Architecture (OO.A4[8]: OO.6.3.3.a)

Activities

Software Design Process Activities (OO.5.2.2.k)
Reviews and Analyses of Software Architecture(OO.6.3.3)

Vulnerabilities

Exception Management (OO.D.1.5)

An exception identifies a condition that is detected by the executing
program (often implicitly by the generated code) and causes aninterruption of the normal control flow and a transfer to a handler. The
condition is typically an error of some sort, for example an out-of-bounds
index.
Exceptions are useful in certain scenarios:102

Frédéric Pothon & Quentin Ochem

When a program deals with externally provided data (operator
input, sensor readings), the exception mechanism is a convenient
way to express validity checks. A handler can perform
appropriate diagnostic / recovery actions.

When an emergency shutdown is needed for a systemcomponent, a “last chance handler” can take the appropriate
measures.

However, the general exception mechanism complicates certification forseveral reasons:Typically, verification should have detected and prevented theexception from occurring in the final code. That is, exceptions
often correspond to violations of preconditions, and such
violations should not occur in verified code.



Since the normal control flow has been abandoned, the program
may be in an instable state (for example with aggregate data
structures not fully updated) and writing an appropriate handler
can be difficultDO-332 / ED-217 specifies that exception handling needs to be taken
into account at the architecture level, but doesn’t provide many moredetails. It also lists vulnerabilities to consider; for example, an exception
might not be handled properly and as a result the program could be leftin an inconsistent state.
The GNAT Pro compiler supplies several strategies concerning exceptions.


Checks can be globally deactivated. By default, execution ofcertain constructs (an out-of-range assignment for example)
generates a run-time check. This can be removed through the p option for the compiler. This should only be done after verifyingthat such checks cannot fail.



If exceptions are kept but are meant to trigger an application
shutdown, they can be connected to a “last chance handler”. This
allows the application to perform the needed finalization, such as

103

AdaCore Technologies for DO-178C / ED-12C

diagnostics and logging, after which it is terminated and possibly
rebooted.


Exceptions can also be locally handled; this is achieved by
specifying
pragma Restrictions (No_Exception_Propagation). This
GNAT-specific restriction ensures that an exception is only raised
when its handler is statically in the same subprogram. Exception
handling can then be implemented (conceptually) by a simple
branch to its handler. Such a policy is much easier to manage in asafe way than general exception propagation. Local handling isuseful in situations where the software requirements specify aparticular termination behavior for a subprogram underconditions that are best detected by raising an exception. An
example is a “saturated add” procedure that takes two positive
integers and delivers a positive integer result and an overflow
status: the integer result will be the actual sum if no overflow
occurred, and the maximum positive value if an overflow
occurred.
type Overflow_Status is (No_Overflow, Overflow);
procedure Saturated_Add (I1, I2 : in Positive;
Result : out Positive;
Status : out Overflow_Status)is
begin
Result := I1+I2;
Status := No_Overflow;
exception
when Constraint_Error =>Result := Integer'Last;
Status := Overflow;
end Saturated_Add;

SPARK addresses the exception handling issue by ensuring thatexceptions are never raised:

104

The SPARK tools can be used to demonstrate the absence of runtime exceptions.

Frédéric Pothon & Quentin Ochem



Handlers are not permitted.



Raise statements are permitted but must be proved to never
execute.

4.3.7.
Overloading and type conversion
vulnerabilities
Contributions
Objectives

Reviews and Analyses of Source Code (OO.A-5[6]:OO.6.3.4.f)

Activities

Reviews and Analyses of Source Code (OO.6.3.4)

Vulnerabilities

Overloading (OO.D.1.3)
Type Conversion (OO.D.1.4)

Many languages allow subprogram overloading (use of the same namefor different subprograms, with a call resolved based on the types of theactual parameters and possibly also the return type for a function) and
implicit type conversions. This combination can lead to readability and/or
maintainability issues. For example, the application may have twofunctions with the same name and the same number of parameters, only
distinguished by their type. In C++ this could be:
int f (int x);
int f (float x);...
int r = f (100);

Knowing which function f() will be called is not immediately obvious.
Furthermore, if the original version of the program contained only the
declaration of f() with a float parameter, and the declaration of f()with an int parameter was added during maintenance, then therecompilation of f(100) would silently change the effect of the program
to invoke the new version of f().

105

AdaCore Technologies for DO-178C / ED-12C

Compiler warnings or static analysis tools are required to identify suchcases and warn the user that a possibly unintended call may be made.
Such problems are much less frequent in Ada, since the language does notallow these sorts of implicit conversions. If a call is ambiguous, this isdetected and the developer will need to specify the intent. Here is an
example:type Milesis new Integer;
type Kilometers is new Integer;function F (Distance : Miles)
return Integer;function F (Distance : Kilometers) return Integer;
R : Integer := F (100);-- Ambiguous

The above code is illegal in Ada due to the ambiguity: the literal 100
could be interpreted as either a Miles or a Kilometers value. A
construct called “type qualification” can be used to make the type explicit
and the call unambiguous:
R1 : Integer := F ( Miles'(100) );R2 : Integer := F ( Kilometers'(100) );With its restrictions on implicit conversions and its provision of an explicit
facility for making subprogram calls unambiguous, Ada supports thenecessary verification activity to mitigate the vulnerabilities in question.

4.3.8.
Accounting for dispatching in
performing resource analysis
Contributions
Objectives

Reviews and Analyses of Source Code (OO.A-5[6]:OO.6.3.4.f)

Activities

Reviews and Analyses of Source Code (OO.6.3.4)

Vulnerabilities

Resource analysis (OO.D.2.4)

106

Frédéric Pothon & Quentin Ochem

One of the difficulties in resource analysis (worst case execution time,
maximal stack usage, etc.) is how to take into account that the target of adispatching call is unknown. This can be addressed by including resource
consumption limits as part of the call requirements. E.g., each overriding
version of a given subprogram must complete within a particular relative
deadline, or use at most a particular amount of stack space. The usual
substitutability rules would then apply; in effect such resource consumption
requirements are a form of postcondition.
The GNATstack tool would provide a more pessimistic approach to worstcase stack computation, and use the maximum value required over all
possible targets in its computation.

107

AdaCore Technologies for DO-178C / ED-12C

4.4. Use case #2: Developing a design model andusing a qualified code generator (QGen)
This use case entails developing the lower level of architecture andrequirements in the form of Simulink® and/or Stateflow® models during
the design process, based on a higher level of requirements. This
representation is considered a “design model” in DO-331 / ED-218 (theModel-Based Development and Verification Supplement). A design model
may be translated directly into source code. In this use case, QGen isused as a qualified code generator, to automatically generate sourcecode in SPARK or MISRA-C from the design model.

4.4.1.
Model development / verification andcode generation
Contributions
Objectives

Software Design (MB.A-2[3,4,5, MB9, MB10]: MB.5.2.1)
Software Coding (A-2[6]: 5.3.1.a)

Activities

Software Design (MB.5.2.2)
Software Coding (5.3.2.d – Autocode)

To apply this use case, a Simulink® and/or StateFlow® design model isdeveloped. One of the main benefits of this approach is the ability todetect potential errors early by verifying the model through model
simulation.
Although most of activities around the development and the verification of
the model are outside the scope of AdaCore solutions, QGen can be used
to help identify certain kinds of errors in the model (see below).
Source code can be generated from the model manually, by a nonqualified code generator, or by a qualified code generator. Eachapproach has benefits and drawbacks:
Manual code generation
108

Advantages

Frédéric Pothon & Quentin OchemoNo need to develop or buy a toolo

Any source code language may be usedoFlexibility in defining source code formatoProblems may be repaired at source code levelo

No constraints in model development

DisadvantagesoWorkload in source code development and verificationoHigh impact of model modifications

Automated code generation with non-qualified toolAdvantagesoAlmost no source code development workload, except
libraries (if any)oProblems may be repaired at source code levelo

No need to qualify the code generator

DisadvantagesoNeed to buy or develop a code generatoroAll source code verification activities need to be
performed, automatically or manuallyoConstraints in model development for tool complianceoLimited choice of source code language and format

Use of a qualified code generator
Advantageso

No source code development workload, except libraries(if any)109

AdaCore Technologies for DO-178C / ED-12CoSignificantly reduced effort in verification activities forsource code, low-level testing and structural coverage
analysis

DisadvantagesoNeed to buy or develop a qualified code generatoroConstraints in model development for tool complianceoChanging the source code entails modifying the modelo

Limited choice of source code language and format

AdaCore’s solution for this use case is the QGen tool, which automates thegeneration of SPARK / Ada or MISRA-C source code from a safe subsetof Simulink® and Stateflow® blocks. This discussion assumes using thequalified version of QGen.
The use of a qualified code generator facilitates a very efficient life
cycle, reducing the effort for a number of verification activities. The next
sections describe a possible strategy to gain credit for QGen in the areasof source code verification (Table A-5, objectives 1-6), low-level testing(A-6, objectives 3-4) and structural coverage analysis (A-7, objectives 57).

4.4.2.

Contributions to model verification
Contributions

Objectives

Reviews and Analyses of Low-Level Requirements (A-4[2]:6.3.2.b)
Reviews and Analyses of Software Architecture (A-4[9]:6.3.3.b)

Activities

Reviews and Analyses of Low-Level Requirements (6.3.2)
Reviews and Analyses of Software Architecture (6.3.3)

QGen uses the same code analysis as CodePeer. Thus a variety ofaccuracy and consistency objectives that are typically verified at sourcecode level (such as freedom from scalar overflows, out-of-range array

110

Frédéric Pothon & Quentin Ochem

indexes, and uses of uninitialized variables) can be verified at the modellevel, ensuring model consistency.
Through qualification, the analysis performed on the model by QGen
provides the necessary confidence that no additional errors have been
inserted in the source code.

4.4.3.
Qualification credit on source code
verification objectives
Contributions
Objectives

Reviews and Analyses of Source Code (MB.A5[1,2,3,4,5,6]: MB.6.3.4.a, MB.6.3.4.b, MB.6.3.4.c,
MB.6.3.4.d, MB.6.3.4.e, MB.6.3.4.f)

Activities

Reviews and Analyses of Source Code (6.3.4)

QGen qualification guarantees that “what is in the model is in the code”.
To justify this claim, qualification includes (among other things) the
following activities

developing accurate tool requirements,

defining the exact source code to be produced for each model
element, andverifying that the code produced for each allowed model
element and combination complies with the tool requirements.

Since tool qualification provides confidence that the generated sourcecode is complete and correct (as a faithful translation of the model), theverification activities on the source code are significantly reduced. For
example the following objectives are met by tool qualification, so theirassociated activities do not need to be performed:source code complies with the requirements (the model),

source code complies with the software architecture (expressed in
the model),111

AdaCore Technologies for DO-178C / ED-12C



source code is verifiablesource code conforms to standards expressed in the qualificationkit,source code is traceable to low level requirements (the model),i.e., all low-level requirements have been implemented in sourcecode (DO-178C / ED-12C §6.3.4.e)

The elimination of these activities applies both at the initial stage (the firsttime code is generated from the model) and subsequently at each
iteration (after the model has been updated for whatever reason).
As previously noted, the DO-178C / ED-12C objective for “Accuracy andconsistency of source code” lists a number of development errors thatneed to be prevented. Some of these, such as unused variables and readsof uninitialized variables, are addressed through tool qualification.
Others are not linked to the translation of requirements into source code,
but rather relate to the integration phase. Examples include target
computer capabilities such as Worst Case Execution Time, memory usage,
stack usage, and arithmetic calculation resolution. These items just need tobe addressed independently of the code generation method. Note thatuse case #1 addresses some of these aspects (e.g., stack size).

4.4.4.
Qualification credit on Executable
Object Code verification objectives
Contributions
Objectives

Software Testing (A-6[3,4]: 6.4.c, 6.4.d)

Activities

Requirement-Based Testing Methods (6.4.3)
Requirement-Based Test Selection (6.4.2, 6.4.2.1, 6.4.2.2)
Software Verification Process Traceability (6.5)

DO-178C / ED-12C requires verifying that the executable object code
complies with all levels of requirements. This is typically accomplishedthrough testing. Since the design model expresses the low-level

112

Frédéric Pothon & Quentin Ochem

requirements, it is necessary to demonstrate that the executable object
code complies with the requirements reflected in the model.
There are several possible approaches, without developing the low-leveltesting based on requirements contained in the model itself. Each has
benefits and drawbacks. The choice depends on the modeling standard(and whether/how it restricts model complexity), the nature of therequirements from which the model was developed, and the capabilitiesof the test environment. Early discussion with the certification authorities is
encouraged. There are two main approaches:Tool qualification credit, as defined in DO-330 / ED-215, FAQ§D.8 scenario 3: “Satisfaction of low-level requirements-based
test objectives through qualification of the ACG (Automatic Code
Generator) and verification of a set of representative input files”
The Tool Operational Verification and Validation activity that ispart of the qualification process offers an equivalent to low-level
requirements-based testing. It involves taking a representative setof input files (models) based on the modeling standard, invoking
the ACG to produce source code, generating the executableobject code (EOC) through the same build environment (compiler,
linker) that is used for the airborne software, and verifying
compliance of the EOC with the representative input files throughtesting that satisfies objectives 1, 2, and 4 in Table A-7 of DO178C / ED-12C.
Tool Operational Verification and Validation is project
dependent, and the activities need to be conducted in the tool
operational environment (DO-330 / ED-215 §6.2.2c). These
activities may be performed either by AdaCore or the QGen
user depending on the context.
A key point in this approach is the choice of the model samples.
To demonstrate that they are representative, the samples must
include all allowed elements (based on the modeling standard),
and combinations of such elements representative of what will
occur in the airborne software. Further, the source code
generated from these samples must include all possible sourcecode constructs that may be generated by the ACG.

113

AdaCore Technologies for DO-178C / ED-12C

The rules in the modeling standard must be sufficiently restrictive
to make this effort manageable, but general enough to express
the required functionality. QGen’s selection of a safe subset of
Simulink® and Stateflow® elements helps strike an appropriatebalance.


Requirement coverage analysis based on high-level testing
As noted above, DO-178C / ED-12C requires verifying that theEOC complies with all levels of requirements. But the standard
also recognizes that if a test developed for a higher-level
requirement satisfies the objectives (including structural coverage)
for a low-level requirement, it is not necessary to duplicate thetest in low-level testing (DO-178C/ED-12C §6.4 Note).
The ability to have the same test serve at multiple levels is
independent of the formalism for developing the requirements
and the method for generating the code. But it is especiallyapplicable in model-based development and verification.

114oA design model is generally verified using model
simulation. As required by DO-331 / ED-218, simulation
cases are developed based on the “requirements fromwhich the model is developed” and thus at a higher level(typically the high-level requirements) than those definedin the design model.

oIn order to detect possible unintended elements in thedesign model, “Model Coverage Analysis” is required.
This analysis consists in identifying the model elements not
exercised during the verification (simulation or tests) andis performed based on the “requirements from which themodel is developed”.

oThe criteria for Model Coverage Analysis are notcompletely defined in DO-331 / ED-218. But if theseinclude the same criteria as those for requirements
coverage analysis, then the verification cases developed
based on the “requirements from which the model isdeveloped” also cover the requirements defined in theFrédéric Pothon & Quentin Ochem

design model. It is then not necessary to duplicate thetests, as long as structural coverage analysis is alsoachieved.
In order for this method to be accepted, the simulation cases
should be converted into test procedures and run on theexecutable object code (see DO-331 / ED-218 FAQ #16). To
perform this re-execution, the code generated by QGen andcompiled with a cross-compiler may be included in the form of an
S-Function in the Simulink® model. Then the outputs from the modeland the S-function may be compared, confirming (or not) that thebinary code is equivalent to the model behavior.

4.4.5. Qualification credit on structural code
coverageContributions
Objectives

Test Coverage Analysis (A-7[5]: 6.4.4.c)

Activities

Structural Coverage Analysis (6.4.4.2.a, 6.4.4.2.b)

Model coverage analysis activities may satisfy structural code coverage
analysis objectives under appropriate conditions. As defined in DO-331 /ED-218 FAQ #11 these conditions include the following:

The applicable structural code coverage analysis criteria apply
to model coverage analysis, for the level of the software being
developed; for example, MC/DC for level A.

Qualification of the code generation tool chain with respect to theobjectives for which certification credit is sought shows that theapplicable coverage properties for the model are preserved forthe code. (The QGen qualification material demonstrates
equivalence between model-level coverage and source-level
coverage. As a result, credit for source code coverage is
obtained from model coverage without the need for any
additional activity beyond qualification.)

115

AdaCore Technologies for DO-178C / ED-12C

116

Any libraries used by code generated from the Design Modelare verified according to DO-178C / ED-12C Section 6(Software Verification Process), including structural code
coverage analysis based on the software level.

Frédéric Pothon & Quentin Ochem

4.5. Use case #3: Using SPARK and formal
analysis
This use case is also a variant of use case #1, since the source code isdeveloped in Ada. It thus benefits from Ada’s advantages and the
AdaCore ecosystem. The difference here is that the contracts, in theSPARK subset of Ada, are used to develop the low-level requirements.
These contracts are amenable to formal analysis by GNATProve, which
can verify consistency with the implementation.

4.5.1. Using SPARK for design data development
Contributions
Objectives

Software Design (A-2[3,4]: 5.2.1.a, 5.2.1.b)
Software Reviews and analyses – Requirement
formalization correctness (FM.A-5[FM12]: FM.6.3.i)
Considerations for formal methods (FM.A-5[FM13]:
FM.6.2.1.a, FM.6.2.1.b, FM.6.2.1.c)

Activities

Software Development Standards (4.5)
Software Design (5.2.2.a, 5.2.2.b)
Software Reviews and analyses – Requirement
formalization correctness (FM.6.3.i)
Considerations for formal methods (FM.6.2.1)

The Ada language in itself is already a significant step forward in termsof software development reliability. However, as a general-purpose
language it contains features whose semantics is not completely specified(for example, order of evaluation in expressions) or which complicate
static analysis (such as pointers). Large applications may need the latter,for example to define and manipulate complex data structures, toimplement low-level functionality, or to interface with other languages.
However, sound design principles should isolate such uses in wellidentified modules, outside a safe core whose semantics is deterministic
and which is amenable to static analysis. This core can be developed with117

AdaCore Technologies for DO-178C / ED-12C

much more stringent coding rules, such as those enforced in the SPARK
language.
SPARK is an Ada subset with deterministic semantics, whose features areamenable to static analysis based on formal methods. For example, it
excludes pointers, exception handling, side effects in functions, andaliasing (two variables referring to the same object at the same time),and guarantees that variables are only read after they have been
initialized. Note that a SPARK program has the same run-time semantics
as Ada. It is compiled with a standard Ada compiler, and can be
combined with code written in full Ada.
SPARK is also a superset of the Ada language in terms of staticallyverified specifications. A variety of pragmas and aspects can be used todefine properties (contracts) such as data coupling, type invariants, andsubprogram pre- and postconditions. These are interpreted by the SPARK
analysis tool and do not have any effect at run-time (and thus they canbe ignored by the compiler, although dynamic verification is allowed forsome) but they can formally document the code and allow further static
analysis and formal proof.
Even without taking advantage of SPARK’s support for formal methods,
coding in SPARK (or using SPARK as the basis of a code standard) helps
make the software more maintainable and reliable. SPARK’s contracts use
the same syntax as Ada, and as just noted, a number of checks that a
SPARK analysis tool could enforce statically can be enabled as run-time
checks using standard Ada semantics, allowing traditional testing-based
verification.
SPARK programs can be verified to have safety and secutity properties
at various levels. At minimum, SPARK analysis can demonstrate absence of
run-time errors/exceptions (such as buffer overrun and integer overflow)
and ensure that variables are assigned to before they are read. In theextreme, SPARK can show that an implementation complies with a formal
specification of its requirements, and this may be appropriate for somecritical kernel modules. Since subprogram pre- and postcondition contracts
often express low-level requirements, some testing of the low-level
requirements may be replaced by formal proofs as described in the DO333 / ED-216 Formal Methods supplement to DO-178C / ED-12C.

118

Frédéric Pothon & Quentin Ochem

In summary, SPARK enhances Ada’s benefits in reducing programming
errors, increasing the quality and effectiveness of code reviews, andimproving the overall verifiability of the code. It facilitates advanced
static analysis and formal proof. At the start of a new development,
considering SPARK for at least part of the application kernel can greatly
decrease defects found late in the process. And when adding functionality
to an existing project, SPARK can likewise bring major benefits since itallows interfacing with other languages and supports combining formal
methods with traditional testing-based verification.
As part of the DO-178C / ED-12C processes, a manual review of therequirements translated into SPARK contracts needs to be conducted.
Although SPARK can ensure that contracts are correctly and consistently
implemented by the source code, the language and its analysis tools
cannot verify that the requirements themselves are correct.
Another issue that needs to be taken into account is the justification of theformal method itself. It should provide a precise and unambiguous
notation, and it needs to be sound (i.e., if it is supposed to identify aparticular property in the source code, such as no reads of uninitialized
variables, then it has to detect all such instances). The qualificationmaterial for the formal analysis tool would typically address this issue.
Moreover, any assumptions concerning the formal method must be
identified and justified.

4.5.2.

Robustness and SPARK
Contributions

Objectives

Software Design (A-2[3,4,5]: 5.2.1.a, 5.2.1.b)

Activities

Software Design (5.2.2.f)

As discussed in Section 4.2.4, robustness is concerned with ensuring correct
software behavior under abnormal input conditions. Abnormal input cancome from two sources:

External: invalid data from the operational environment (forexample due to an operator input error or a hardware failure),or
119

AdaCore Technologies for DO-178C / ED-12C

Internal: a defect in the software logic.

Behavior in the external case needs to be considered during requirements
development, and from the SPARK perspective (where these requirements
are captured as pre- or postconditions) there is no fundamental
difference between a regular requirement and a robustness requirement.
The proof performed by SPARK takes into account the entire potential
input space, whether normal or abnormal.
The internal case, where faulty code passes an invalid value to a
subprogram, can be detected by SPARK (GNATprove) if the validity
requirement is part of the subprogram’s precondition. That is, GNATprove
will report its inability to prove that the subprogram invocation satisfies
the precondition.

4.5.3.
Contributions to Low Level
Requirement reviews
Contributions
Objectives

Reviews and Analyses of Low-Level Requirements (FM.A4[2,4,5]: FM.6.3.2.b, FM.6.3.2.d, FM.6.3.2.e)
Reviews and analyses of formal analysis cases, procedures
and results (FM.A-5[FM10,FM11]: FM.6.3.6.a, FM.6.3.6.b,
FM 6.3.6.c)

Activities

Reviews and Analyses of Low-Level Requirements(FM.6.3.2)
Reviews and analyses of formal analysis cases, procedures
and results (FM.6.3.6.)

Using SPARK to define low-level requirements (LLRs) simplifies theverification process. Since the LLRs are expressed in a formal language(Ada 2012 or SPARK contracts), by definition they are accurate,unambiguous, and verifiable: expressed as Boolean expressions that canbe either tested or formally proven.
SPARK also makes it easier to define a software design standard, which
can use the same terms and concepts as a code standard, and can bechecked with similar tools.

120

Frédéric Pothon & Quentin Ochem

4.5.4.

Contributions to architecture reviews
Contributions

Objectives

Reviews and Analyses of Software Architecture (FM.A4[9,11,12]: FM.6.3.3.b, FM.6.3.3.d, FM.6.3.3.e)

Activities

Software Development Standards (4.5)
Reviews and Analyses of Software Architecture (FM.6.3.3)

According to DO-333 / ED-216, the reviews and analyses of thesoftware architecture “detect and report errors that may have been
introduced during the development of the software architecture”. SPARK
helps meet several of the associated objectives:


Consistency. SPARK’s flow analysis contracts can specify various
relationships between the software components, including acomponent’s data dependencies and how its outputs depend on
its inputs. The SPARK analysis tool (GNATprove) can then verify
the correctness of these contracts / relationships, assuming TQL-5
qualification, and the consistency of the architecture. For
example:type Probe_Type isrecord...
end record;
Probes : array (1 .. 10) of Probe_Type;procedure Calibrate_Probe (Index : Integer;
Min, Max : Integer)
with Globals =>(In_Out => Probes),
Depends =>(Probes => (Probes, Index, Min, Max));

The Calibrate_Probe procedure will use the global variable
Probes in in out mode (it can read from and write to thevariable) and will compute its new value using the old value ofProbes (at the point of call) together with the parameters Index,
121

AdaCore Technologies for DO-178C / ED-12C

Min and Max. SPARK will verify that the only global variable
used is Probes, and that this variable and the parametersspecified in the Depends aspect (and no other variables) areused to compute the value.


Verifiability. As a formal notation with tool support, SPARK canhelp ensure that the architecture is verifiable. One example is theprotection against one component sending invalid input toanother. As noted earlier, this is part of the robustness
requirement that is met by SPARK’s pre- and postconditions.
Keeping these contracts active even in the final executable object
code will protect a component from sending or receiving invalid
input, and will detect any misuse.

Conformance with standards. An architecture standard can be
defined in part using similar formalisms as a code standard, thus
allowing the use of similar tools for verification.

4.5.5.

Contributions to source code reviews
Contributions

Objectives

Reviews and Analyses of Source Code (FM.A-5[1,2,3,6]:
FM.6.3.4.a, FM.6.3.4.b, FM.6.3.4.c, FM.6.3.4.f)

Activities

Software Development Standards (4.5)
Reviews and Analyses of Source Code (FM.6.3.4)

The SPARK analysis tool (GNATprove) can verify that the source code
complies with its low-level requirements (LLRs) defined as SPARK contracts.
This can satisfy the source code verification objectives, depending on thepart of the design data formally defined:Compliance with the LLRs: code is proven against the LLRs



Compliance with the architecture: code is proven against thearchitectural properties defined at the specification level

Verifiability: if the code is verified by SPARK, it is verifiable. No
specific activity is needed here.

122

Frédéric Pothon & Quentin Ochem



Traceability: traceability is implicit, from the LLRs defined in thespecification to the implementation

The SPARK tool achieves proof in a local context; it’s doing a “unit proof”.
The postcondition of a subprogram will be proven according to its codeand its precondition, which makes the SPARK approach scalable. For
example, consider the following function:
type My_Array is array(Positive range <>) of Integer;function Search (Arr
: My_Array;
Start : Positive;
Value : Integer)
return Integer
with Pre =>Start in Arr'Range,
Post =>(if Search'Result = -1 then(for all I in Start .. Arr'Last => Arr (I) /= Value)else Arr(Search'Result) = Value);

The code inside the body might start with:function Search (Arr
: My_Array;
Start : Positive;
Value : Integer)
return Integer is
begin
if Arr (Start) = Value thenreturn Start;
end if;...

Because of the precondition, the SPARK analysis tool can deduce that thearray indexing will not raise an exception.
Here’s another piece of code, responsible for replacing all occurrences of
one value by the other:123

AdaCore Technologies for DO-178C / ED-12C

procedure Replace (Arr : in out My_Array;
X, Y : in Integer)
with Pre => Arr'Length /= 0 and X /= Y,
Post => (for all I in Arr'Range =>(if Arr'Old (I) = X then Arr (I) = Y));procedure Replace (Arr : in out My_Array; X, Y : Integer) is
Ind : Integer := Arr'First;
begin
loop
Ind := Search (Arr, Ind, X);
exit when Ind = -1;
Arr (Ind) := Y;exit when Ind = Arr'Last;
end loop;end Replace;

When Search is invoked, the only things that the prover knows are its
pre- and postconditions. It will attempt to show that the precondition issatisfied, and will assume that the postcondition is True. Whether or not
Search is proven doesn’t matter at this stage. If it can’t be proven with
the SPARK tools, we may decide to verify it through other means, such as
testing.
The SPARK analysis tools can demonstrate absence of run-time errors,
absence of reads of uninitialized variables, absence of unused
assignments, and other properties. Additional contracts may sometimes beneeded for assistance (e.g., assertions), but overall SPARK’s restrictedfeature set and advanced proof technology automate contract proofs
with very few cases needing to be manually dismissed. This almost
entirely replaces manual reviews and analyses.
The analysis performed by SPARK is usually very tedious to conduct bymanual review. As an example, here’s a simple piece of code:124

Frédéric Pothon & Quentin Ochem

subtype Some_Int is Integer range ...;
Arr : array (Integer range <>) of Some_Int := ...;
Index, X, Y, Z : Integer;...
Arr (Index) := (X * Y) / Z;

Exhaustive analysis of all potential sources of errors requires verifyingthat:

X is initializedY is initialized

Z is initializedIndex is initialized and is in Arr'Range(X * Y) does not overflow

Z is not equal to zero(X * Y) / Z is within Some_Int

The SPARK tools will check each of these conditions, and report any thatmight not hold.

4.5.6.
Formal analysis as an alternative to lowlevel testing
Contributions
Objectives

Software Testing (A-6[3,4]: 6.4.c, 6.4.d)

Activities

Low Level testing (6.4.3.c)

The purpose of testing in DO-178C / ED-12C is to check that theexecutable object code complies with its requirements. Thus it’s not thesource code but the binary code that is tested, and within an environment
representative of the final target. As a consequence, the compiler itself is125

AdaCore Technologies for DO-178C / ED-12C

not part of the trusted chain. Since its outputs are verified, it can beassumed to be correct within the exact conditions of the certified
application.
Various activities in DO-178C / ED-12C increase the confidence in thecompilation step, such as selecting an appropriate set of options,assessing the effect of its known problems and limitations, and (atsoftware level A) verifying the correctness of non-traceable code
patterns.
DO-333 / ED-216 explains how certain classes of testing can be
replaced by formal analysis (“proof”). When low level requirements are
expressed as formal properties of the code, it’s possible to formallyverify that the source code completely implements the requirements. Using
this technique, however, requires additional activities to demonstrateabsence of unintended function. Further, and more significantly, withformal analysis it’s the source code that is checked against requirements,
not the object code. As a result, additional activities are required todemonstrate correct behavior of the object code. This is the so-called“property preservation”, discussed later.
Overall, formal analysis can offer better error detection through its
exhaustive checks. But if credit is sought for executable object code
verification, Tool Qualification Criterion 2 in DO-178C / ED-12C §12.2.2
applies to the formal analysis tool: the analysis tool’s output is being used
“to justify the elimination or reduction of verification process(es) other thanthat automated by the tool”. In consequence, GNATprove is qualified at
TQL-4 to be usable at all software levels.

4.5.7.
Low level verification by mixing test
and proof (“Hybrid verification”)
Contributions
Objectives

Software Testing (A-6[3,4]: 6.4.c, 6.4.d)

Activities

Low Level testing (6.4.3.c)126

Frédéric Pothon & Quentin Ochem

It is not always possible for the SPARK proof tool to prove all thecontracts in an application. When this is due to limited capabilities in the
proof technology, manually provided assistance may be a solution.
However, some assertions and contracts might not be provable at all. This
could be due to several factors:
The specification is in SPARK but the actual implementation is in adifferent language (such as C).

The contract or implementation uses Ada features outside of theSPARK subset.

Some constructs might not be amenable to formal proof, even if
correct, because a piece of code is too complex.

Some final proof step may be hard to reach, requiring an effort
that is excessive compared to some other verification technique.

For all of these reasons, a combination of proof and testing may beappropriate to fully verify the software. The basic principle is that SPARK
proofs are local. They’re performed assuming that each called
subprogram fulfills its contracts: if its precondition is satisfied and thesubprogram returns, then its postcondition will hold. If this correctness isdemonstrated by formal proof, then the whole program is proven tocomply with all contracts. However, correctness may also bedemonstrated by testing. In this case, the dual semantics of contracts,
dynamic and static, is key. The pre- and postconditions can be enabled as
run-time checks to verify the expected output of the test procedures.
An efficient approach during the design process is to define anarchitecture that distinguishes between those components verified byformal proofs and those verified by testing. Mixing the two techniques issometimes referred to as “hybrid verification”.

127

AdaCore Technologies for DO-178C / ED-12C

4.5.8.
Alternatives to code coverage whenusing proofs
Contributions
Objectives

Principles of Coverage Analysis when using Formal Methods(FM.A-7[FM5-8]: FM.6.7.1.c)

Activities

Requirement-Based Coverage Analysis (FM.6.7.1.2,
FM.6.7.1.3, FM.6.7.1.4, FM.6.7.1.5)

Structural code coverage is a test-based activity for verifying theexhaustivity of the testing, the completeness of the requirements, and theabsence of unintended function (extraneous code, including dead code).
With formal proofs, a different set of activities is needed to meet similar
objectives. DO-333 / ED-216 lists four activities to be performed:
Complete coverage of each requirement. This objective is toverify that each assumption made during the analysis is verified.
In SPARK, these assumptions are easily identifiable. These are
typically assertions in the code that cannot be provenautomatically, for example because they are too complex or
involve interfacing with non-SPARK code. These assumptions canbe verified not with proofs but with alternative means such as
testing and reviews.

Completeness of the set of requirements. In particular, for each
input condition its corresponding output condition has been
specified, and vice versa. This can be achieved, for example, byspecifying dependency relationships between input and output(the SPARK aspect Depends) or by partitioning the input space(the SPARK aspect Contract_Case).



Detection of unintended dataflow relationships. The SPARK
aspect Depends will verify that each output is computed from its
specified set of inputs.



Detection of extraneous code. If the requirements are complete
and all output variables (and their dependencies) are specified in

128

Frédéric Pothon & Quentin Ochem

these requirements, then any extraneous code should be deadand have no unintended effect. A manual review of the code will
help achieve confidence that no such code is present.

4.5.9.
Property preservation between sourcecode and object code
Contributions
Objectives

Verification of Property Preservation Between Source andExecutable Object Code (FM.A-7[FM9]: FM.6.7.f)

Activities

Verification of Property Preservation Between Source andExecutable Object Code (FM.6.7.f -1)

When part of the executable object code (EOC) verification is performed
using formal proof instead of testing, the source code is verified against
the requirements, but the compiler is out of the loop. As a result,additional activities need to be performed to confirm proper translationof the source code to object code.
This is an open topic, and several approaches are possible to achieve
credit for preservation of properties. One possibility is to perform an
analysis of the compiler’s processing similar to the source-code-to-objectcode traceability study that addresses DO-178C / ED-12C §6.4.4.2.b.
However, in addition to analyzing and justifying instances of nontraceability, the behavior of traceable code also needs to be considered/ verified.
An alternative solution is to rely on the fact that SPARK functional
contracts are executable Ada expressions. These are the actual
properties that need to be preserved between source code and EOC.
One way to demonstrate property preservation is to run the tests basedon a higher level of requirements (such as Software / Software
integration testing) once, with contract checks activated. If no contract
failure occurs, we can conclude that the expected behavior has been
properly translated by the compiler. This gives sufficient confidence in thecode generation chain.
129

AdaCore Technologies for DO-178C / ED-12C

Running tests to verify this activity may seem to defeat the purpose of
replacing testing by proof. However, this should not be considered as
requirement-based testing (which is indeed replaced by proof). This
“property preservation” verification is a confirmation of the formal
analysis by executing the EOC with contract checking enabled.

4.6. Parameter Data Items
Contributions
Objectives

Software requirements process (A-2[1]: 5.1.1.a)
Software integration process (A-2[7]: 5.4.1.a)
Verification of Parameter Data Items (A-5[8,9]: 6.6)

Activities

Software requirements process (5.1.2.j)
Software Integration process (5.4.2.a)
Verification of Parameter Data Items (6.6.a), (6.6.b)

The term “Parameter Data Item” (PDI) in DO-178C / ED-12C refers to aset of parameters that influences the behavior of the software without
modifying the Executable Object Code. The verification of a parameterdata item can be conducted separately from the verification of the
Executable Object Code.
PDI development implies the production of three kinds of data:The “structure and attributes”: These define the characteristics ofeach item, such as its type, range, or set of allowed values. In
order to ensure the data item correctness and consistency, a setof consistency rules should also be defined. For example, if one
item defines the number of temperature sensors, and other items
define the characteristics of each sensor, there is an obvious
relationship between these items.

The specification of an instance of a PDI: The defined set ofvalues for each item for an applicable configuration

The PDI file that implements an instance of a PDI directly usableby the processing unit of the target computer (e.g. a binary file)An efficient way to develop such artifacts is to use Ada and/or SPARK.
130

Frédéric Pothon & Quentin Ochem

The structure and attributes can be defined in one or more package
specifications. Each item is defined with its type, defining range and set ofallowed values. Predicates can be used to define relationships between
parameters. The example below combines a classical approach using
strong typing and type ranges, with a dynamic predicate to describe
relationships between components of the structure. The intent is to specify
the accepted range of temperatures for a given sensor.
type Sensor isrecordMin_Temp : Float range -40.0 .. 60.0;
Max_Temp : Float range -20.0 .. 80.0;
end record
with Dynamic_Predicate => Sensor.Min_Temp < Sensor.Max_Temp;

Each PDI instance needs to satisfy the constraints expressed in the
Dynamic_Predicate aspect. These constraints are based on a higherlevel specification, such as customer-supplied requirements, a system
configuration description, or an installation file. Generating the PDI filefor an instance consists in using GNAT Pro to compile/link the Ada sourcecode for the PDI, producing a binary file.
Verifying the correctness of a PDI instance (compliance with structure andattributes) can be automated by compiler checks. This means thatinconsistencies will be detected at load time. For example,
S1 : Sensor := (Min_Temp => -30.0, Max_Temp => 50.0);
S2 : Sensor := (Min_Temp => -50.0, Max_Temp => 50.0);
S3 : Sensor := (Min_Temp => 40.0, Max_Temp => 30.0);

S1 will be accepted, S2 will not (Min_Temp is out of range), S3 will not(Min_Temp is above Max_Temp). (The Dynamic_Predicate check canalso be enabled as a run-time check, via pragma
Assertion_Policy(Check) and the -gnata switch to the GNAT
compiler.) If all PDIs are defined in this manner, completeness ofverification is ensured.
The only remaining activity is to check that the PDI instance value complies
with the system configuration.

131

AdaCore Technologies for DO-178C / ED-12C

132

Frédéric Pothon & Quentin Ochem

5. Summary of contributions
to DO-178C/ED-12C
objectives
5.1 Overall summary: which objectives are met
The following table summarizes how the Ada and SPARK languages and
AdaCore’s tools help meet the objectives in DO-178C / ED-12C and thetechnology supplements. The numbers refer to the specific objectives in thecore document or the relevant supplement.
Table A-3 and Tables A-8 through A-10 are not included since they are
independent of AdaCore’s technologies.

133

AdaCore Technologies for DO-178C / ED-12C

Overall Summary
Which DO-178C objectives are met by AdaCore’s Technologies

134

Frédéric Pothon & Quentin Ochem

5.2 Detailed summary: which activities aresupported
In the tables below, the references in the Activities column are to sectionsin DO-178C / ED-12C or to one of the technology supplements. The
references in the Use case columns are to sections in this document.
Since AdaCore’s tools mostly contribute to the bottom stages of the ”V”
cycle (design, coding, integration and related verification activities),
verification of High-Level Requirements (and thus Table A-3) are outside
the scope of AdaCore solutions.
Likewise, the objectives in Table A-8 (Configuration Management), A-9(Quality Assurance) and A-10 (Certification Liaison Process) are
independent of AdaCore’s technologies; they are the responsibility of the
user.

135

AdaCore Technologies for DO-178C / ED-12C

Table A-1 Software Planning Process

136

Frédéric Pothon & Quentin Ochem

137

AdaCore Technologies for DO-178C / ED-12C

Table A-2 S oftware De velopme nt Proce sse s
AdaCore tools mostly c ontribute t o the bott om s tages of the traditional ”V ” cy cle ( design, co ding, inte gration, and the rel ate d verification activities).

138

Frédéric Pothon & Quentin Ochem

Table A-4 Verificati on of Out put s of S oftware De si gn Proce ss

Table A-5 Verificati on of Out put s of S oftware Coding & Inte grati on Proce sse s139

AdaCore Technologies for DO-178C / ED-12C

140

Frédéric Pothon & Quentin Ochem

Table A-6 Te sting of Out put s of I ntegrat ion Process141

AdaCore Technologies for DO-178C / ED-12C

Table A-7 Verification of Verification Process Results142

Frédéric Pothon & Quentin Ochem

143

AdaCore Technologies for DO-178C / ED-12C

References[1]

Yannick Moy, Emmanuel Ledinot, Hervé Delseny, Virginie Wiels,
Benjamin Monate, “Testing or Formal Verification: DO-178C
Alternatives and Industrial Experience”, IEEE Software, 2013.

[2]

ISO/IEC, Ada Language Reference Manual, 2012.
Available at www.adaic.org/ada-resources/standards/ada12/[3]

John Barnes and Ben Brosgol, Safe and Secure Software, aninvitation to Ada 2012, AdaCore, 2015.
Available at www.adacore.com/knowledge/technicalpapers/safe-and-secure-software-an-invitation-to-ada-2012/[4]

John Barnes, Programming in Ada 2012, Cambridge University
Press, 2014

[5]

AdaCore, High-Integrity Object-Oriented Programming in Ada,
2013. Available at www.adacore.com/knowledge/technicalpapers/high-integrity-oop-in-ada/[6]

John W. McCormick and Peter C. Chapin, Building High Integrity
Applications with SPARK, Cambridge University Press, 2015

[7]

Paul E. Black, Michael Kass, Michael Koo, Elizabeth Fong, Source
Code Security Analysis Tool Functional Specification, NIST, 2011.

[8]

Matteo Bordin, Cyrille Comar, Tristan Gingold, Jérôme Guitton,
Olivier Hainque, Thomas Quinot, Object and Source Coverage for
Critical Applications with the COUVERTURE Open Analysis
Framework, ERTS, 2010

[9]

Johannes Kanig, Quentin Ochem, Cyrille Comar, Bringing SPARK
to C developers, ERTS, 2016[10]

Kelly J. Hayhurst, Dan S. Veerhusen, John J. Chilenski, Leanna K.
Rierson; A Practical Tutorial on Modified Condition / Decision
Coverage; NASA / TM-2001-210876; May 2001.

144

Frédéric Pothon & Quentin Ochem

Index

A
Ada language
Arrays, 50
Assertion_Error exception, 24,
66
Buffer overflow prevention, 26
C interfacing, 49, 62
Concurrent programming (tasks), 25
Contract-based programming, 24,
27, 56
Contributions to DO-178C/ED-12C
activities, 45
Dynamic dispatching, 90
Dynamic_Predicate aspect, 131
Generic templates, 25
Hardware/software interfaces, 58
History and overview, 22
Low-level facilities, 51
Numeric types, 61
Object-Oriented Programming(OOP), 25'Old attribute (in a postcondition),
57
OOT vulnerabilities, 18, 86
Overloading example, 106
package Interfaces, 58
package Interfaces.C, 62
Parameter passing, 48
Pointers (access types), 48
Post aspect, 92
Post'Class aspect, 92
Postconditions, 24, 55
pragma Assertion_Policy, 66,
131
pragma Restrictions, 27, 104
Pre aspect, 92
Pre'Class aspect, 92
Preconditions, 24, 56
Programming in the large, 24
Real-Time Systems Annex, 26
Representation clauses, 59
Scalar ranges, 23

Scalar_Storage_Order aspect,
59
Storage_Size attribute (toprevent dynamic allocation), 101
Strong typing, 45
Systems Programming Annex, 26
Traceability analyses (source toobject), 85
Usage, 22
Usage during the design process, 52
Usage for component identification,
53
Usage for defining interfaces, 53'Valid attribute, 60
AdaCoreAda and C integration, 62
Ada history, 22
ASIS-for-GNAT. See ASIS-for-GNAT
CodePeer. See CodePeer
GNAT Pro Assurance. See GNAT Pro
Assurance
GNAT Pro compiler, 63
GNAT Programming Studio. See
GNAT Programming Studio (GPS)GNAT2XML. See GNAT2XML
GNATbench. See GNATbench
GNATcheck. See GNATcheck
GNATcoverage. See GNATcoverage
GNATdashboard. See
GNATdashboard
GNATemulator. See GNAtemulator
GNATmetric. See GNATmetric
GNATprove. See GNATprove
GNATstack. See GNATstack
GNATtest. See GNATtest
SPARK Pro. See SPARK Pro
Support and expertise, 31
Sustained branch. See SustainedbranchASIS (Ada Semantic Interface
Specification), 32
ASIS-for-GNAT, 32
AUnit, 36

145

AdaCore Technologies for DO-178C / ED-12C

B
Babbage, Charles, 22
Buffer overflow, 26, 32

CC language, 12Buffer overflow, 26
Example: pointer arithmetic, 49
Integration with Ada, 62
Supported by GNAT Pro, 29, 71
Traceability analyses (source toobject), 85
C++ language, 62
Buffer overflow, 26
Overloading example, 105
CENELEC EN 50128, 26, 40
Chicago Convention, 14
COBOL language
Interfacing with Ada, 62
Code standard, 43
Enforcement by GNAT2XML, 67
Enforcement by GNATcheck, 33, 67
CodePeer, 31, 43, 66
Checking source code accuracy andconsistency, 69
Common Weakness Enumeration(CWE) errors detected, 32
Early error detection, 31
Qualified as Verification Tool (DO178B/ED-12B), 32
Support for all versions of Ada, 69
TQL-5 qualification, 66, 69
Common Criteria, 26
Common Weakness Enumeration (CWE)
errors detected by CodePeer, 32
Component-based development (OOTand related techniques vulnerability),86
Contract-based programming, 56
Control coupling, 82
Dynamic dispatching, 98

D
Data coupling, 82

146

Dynamic dispatching, 98
Decision coverage, 37, 78
Design Assurance Level, 15
DO-178C/ED-12C
High-Level Requirements. See HighLevel Requirements (HLR)
Low-Level Requirements. See LowLevel Requirements (LLR)
Parameter Data Items, 130
QGen and TQL-1, 40
Source code accuracy andconsistency, 69
Structural coverage analysis, 78
Verification, 20
DO-248C/ED-94C: Supporting
Information for DO-178C/ED-12C
and DO-278A/ED-109A, 15
DO-278A/ED-109A: Software Integrity
Assurance Considerations forCommunication, Navigation,
Surveillance and Air Traffic
Management (CNS/ATM) Systems,
15
DO-330/ED-215: Tool Qualification
Considerations, 12, 16
QGen qualification, 41, 44, 111
DO-331/ED-218: Model-Based
Development and Verification, 13, 18,
44, 108
Model coverage analysis, 114
Model simulation, 114
DO-332/ED-217: Object-Oriented
Technology and Related Techniques,13, 17, 86
Vulnerability Analysis annex, 17
DO-333/ED-216: Formal Methods, 13,
19, 44, 95
Code coverage activities, 128
Dynamic dispatching (OOT), 89
Module coupling, 98
Resource analysis, 106
Dynamic memory management (OOT
vulnerability), 86, 99
DynamoRIO, 81

Frédéric Pothon & Quentin Ochem

E
Eclipse support. See GNATbench
Exception management (OOT andrelated techniques vulnerability), 86,102
Executable Object Code (EOC), 20, 42

FFormal methods
Code coverage, 128
Justification of usage, 119
Replacement for testing, 20, 125
Verifying substitutability (OOT), 95
Fortran language
Interfacing with Ada, 62

G
Garbage collection, 25, 62, 99
Generic templates
Coverage analysis, 87
OOT and related techniques
vulnerability, 86
Traceability, 89
GNAT Pro
Compiler, 71
Dimension_System aspect, 47
Dimensionality checking, 47
Exception handling strategies, 103
Test_Case aspect, 74
GNAT Pro Assurance, 17, 29
Configurable Run-Time Library, 30
Safety analysis of known problems
list, 71
Sustained branch. See SustainedbranchTraceability analysis service. See
Traceability (Source to Object)
GNAT Programming Studio (GPS), 29,
38
GNAT2XML, 33, 68
GNATbench, 30, 39
GNATbus, 77
GNATcheck, 33, 43, 68
Code standard enforcement, 33

TQL-5 qualification, 69
GNATcoverage, 37, 41, 43
Support for data and control
coupling coverage, 82
Support for generic templates, 89
Support for structural code
coverage, 78
TQL-5 qualification, 82
GNATdashboard, 39, 68
GNATemulator, 37, 41, 81
Support for low-level and software/ software integration tests, 76
GNATmetric, 33
GNATprove, 27, 117, 120, 121, 122
TQL-4 qualification, 126
GNATstack, 34, 43, 70, 107
TQL-5 qualification, 70
GNATtest, 36, 43
Support for generic templates, 89
Support for low-level testing, 72
Support for substitutability testing(OOT), 95
GNU GCC technology, 29HHigh-Level Requirements (HLR), 42
Hybrid verification, 29, 126

I
Ichbiah, Jean, 22
Incorrect calculation of buffer size, 32
Integer overflow or wraparound, 32
Integrated Development Environments(IDEs), 38
ISO 26262, 40

JJava language, 25, 62, 100

L
Liskov Substitution Principle (LSP), 37,
90

147

AdaCore Technologies for DO-178C / ED-12C

Local type consistency (OOT
vulnerbility), 86
Lovelace, Augusta Ada, 22
Low-Level Requirements (LLR), 42, 56
Expressed as Ada or SPARK
contracts, 120
Formal methods and source code
compliance, 126
Lynx178 (supported by GNAT Pro), 71

M
Memory management. See Dynamic
memory management (OOT
vulnerability)
MISRA-C
Generated by QGen, 19, 40, 44,108
Model-Based Development
Usage with AdaCore tools, 44
Modified Condition/Decision Coverage(MC/DC), 37, 78

N
Nexus interface, 81

OObject-Oriented Technology
Dynamic dispatching. See Dynamic
dispatching (OOT)
Software architecture definition, 86
Substitutability. See Substitutability(OOT)
Traceability, 87
Usage with AdaCore tools, 43
Verifying substitutability, 94, 95
Vulnerabilities, 86
Options. See Switches
Overloading (OOT and related
techniques vulnerability), 86, 105P
Parameter Data Items, 130
Pessimistic testing (OOT, 94

148

PikeOS (supported by GNAT Pro), 71
Property preservation between sourcecode and object code, 129Q
QEMU, 37
QGen, 13, 19, 39, 108
Executable Object Code verification,
112
Model debugger, 19
Qualification activities, 113
Qualification benefits, 111
Qualification material, 40
Structural code coverage, 115
Support for model static analysis, 41
Support for model verification, 110
Support for Processor-in-the-Loop
testing, 41

R
Ravenscar Profile, 27, 51
Robustness / defensive programming,
63
Ada contracts, 64
SPARK, 119S
S-Function (Simulink®), 115
Simulink®, 13, 18, 19, 39, 108, 114
Software level. See Design Assurance
Level
Software life cycle, 11, 42
SonarQube, 68
Soundness (formal analysis property),
19, 119SPARK, 20, 27, 44
Absence of run-time exceptions, 28,
118, 124
Architecture review support, 121
Buffer overrun prevention, 118
Code compliance with formal
specification, 118
Code coverage, 128
Contract_Case aspect, 128

Frédéric Pothon & Quentin Ochem

Contract-based programming, 56
Data and control flow analysis, 28
Depends aspect, 57, 128
Design data development, 117
Generated by QGen, 19, 44, 108
Global aspect, 57
Information flow analysis, 28
Integer overflow prevention, 118
Integration with C, 63
Language restrictions, 118
Postconditions, 120, 123
Preconditions, 120, 123
Prohibition of exceptions, 104
Property preservation between
source code and object code,
129
Robustness, 119
Source code review support, 122
Static verification support, 28
Support for Low Level Requirement
reviews, 120
Testing replaced by formal proofs,
118
Uninitialized-variable read
prevention, 118, 124
Unused-assignment prevention, 124
Usage, 27
Verifying substitutability (OOT), 95
SPARK Pro, 27
SQUORE, 68
Stateflow®, 13, 19, 39, 108, 114
Statement coverage, 37, 78
Structural testing, 64
Substitutability (OOT), 89, 90
Local versus global, 96
Sustained branch, 29, 30
Switches-fdump-ada-spec (g++), 62-gnata (gcc), 66, 131-gnatceg (gcc), 62--validate-type-extensions(gnattest), 95
SysSML, 18

T
Table A-1 Software Planning Process,67, 136
Table A-2 Software Development
Processes, 45, 52, 62, 63, 67, 71,
86, 89, 99, 102, 108, 117, 119,130, 138
Table A-4 Verification of Outputs ofSoftware Design Process, 52, 110,139
Table A-5 Verification of Outputs ofSoftware Coding & Integration
Processes, 45, 52, 63, 67, 69, 70,
71, 130, 140
Table A-6 Testing of Outputs ofIntegration Process, 72, 76, 112,
125, 126, 141
Table A-7 Verification of Verification
Process Results, 72, 78, 82, 84, 87,
98, 99, 115, 142
Table FM.A-4 Verification of Outputs ofSoftware Design Process, 120, 121
Table FM.A-5 Verification of Outputs ofSoftware Coding & Integration
Processes, 117, 122
Table FM.A-7 Verification of
Verification Process Results, 128,
129
Table MB.A-2 Software Development
Processes, 108
Table MB.A-5 Verification of Outputs ofSoftware Coding & Integration
Processes, 111
Table OO.A-4 Verification of Outputsof Software Design Process, 99, 102
Table OO.A-5 Verification of Outputsof Software Coding & Integration
Processes, 105, 106
Table OO.A-7 Verification of
Verification Process Results, 89
Taft, Tucker, 22
Testing
Pessimistic testing (OOT), 94
Replacement by formal proofs, 125
Requirement-based testing (OOT),
95

149

AdaCore Technologies for DO-178C / ED-12C

Tool Qualification Level (TQL), 16
Traceability (Source to Object), 30, 71,
84
Type certificate (for airworthiness), 14
Type conversion (OOT and related
techniques vulnerability), 86, 105U
UML, 18, 86
Use case #1a: Coding with Ada 2012,45
Use case #1b: Coding with Ada using
OOT features, 86
Use case #2: Developing a designmodel and using a qualified code
generator (QGen), 108

150

Use case #3: Using SPARK and formal
analysis, 117VV software life cycle, 42Valgrind, 38, 81
VxWorks 6 Cert (supported by GNAT
Pro), 71
VxWorks 653 (supported by GNAT
Pro), 71

W
Workbench (WindRiver development
environment), 39