Skip to content

Commit 8038b03

Browse files
Fabien-ChouteauFabien-Chouteau
committed
First version of the Airborne Software Booklet
1 parent 71c60de commit 8038b03

File tree

15 files changed

+4819
-1
lines changed

15 files changed

+4819
-1
lines changed

‎content/booklets/adacore-technologies-for-airborne-software/analysis.rst

Lines changed: 3180 additions & 0 deletions
Large diffs are not rendered by default.

‎content/booklets/adacore-technologies-for-airborne-software/common_defs.rst

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
.. |reg| unicode:: U+00AE .. registered trademark (R)
2+
.. |bullet| unicode:: U+2022
3+
.. |tab| unicode:: U+0009
4+
.. |nl| unicode:: U+000A .. New Line
5+
.. |sect| unicode:: U+00A7
6+
.. |nbsp| unicode:: U+00A0 .. non-breaking space
7+
.. |blank| unicode:: U+0020 .. For use in csv tables, to make empty cell content explicit
8+
.. |nbhyphen| unicode:: U+2011 .. non-breaking hyphen
9+
:trim:
10+
11+
.. |gnata| replace:: "|nbhyphen| gnata"
12+
.. |do-160| replace:: DO |nbhyphen| 160/ED |nbhyphen| 14
13+
.. |do-178| replace:: DO |nbhyphen| 178/ED |nbhyphen| 12
14+
.. |do-178b| replace:: DO |nbhyphen| 178B/ED |nbhyphen| 12B
15+
.. |do-178c| replace:: DO |nbhyphen| 178C/ED |nbhyphen| 12C
16+
.. |do-248b| replace:: DO |nbhyphen| 248B/ED |nbhyphen| 94B
17+
.. |do-248c| replace:: DO |nbhyphen| 248C/ED |nbhyphen| 94C
18+
.. |do-254| replace:: DO |nbhyphen| 254/ED |nbhyphen| 80
19+
.. |do-278a| replace:: DO |nbhyphen| 278A/ED |nbhyphen| 109A
20+
.. |do-326a| replace:: DO |nbhyphen| 326A/ED |nbhyphen| 202A
21+
.. |do-356a| replace:: DO |nbhyphen| 356A/ED |nbhyphen| 203A
22+
.. |do-330| replace:: DO |nbhyphen| 330/ED |nbhyphen| 215
23+
.. |do-331| replace:: DO |nbhyphen| 331/ED |nbhyphen| 218
24+
.. |do-332| replace:: DO |nbhyphen| 332/ED |nbhyphen| 217
25+
.. |do-333| replace:: DO |nbhyphen| 333/ED |nbhyphen| 216
26+
.. |gnatsas| replace:: GNAT SAS
27+
.. |gnatdas| replace:: GNAT DAS

‎content/booklets/adacore-technologies-for-airborne-software/conf.ini

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
[DEFAULT]
2+
title=AdaCore Technologies for Airborne Software
3+
author=Frédéric Pothon \\and Quentin Ochem
4+
version=2.1

‎content/booklets/adacore-technologies-for-airborne-software/images/analysis-fig3.png

18.3 KB
Loading

‎content/booklets/adacore-technologies-for-airborne-software/images/introduction-fig1.png

51.6 KB
Loading

‎content/booklets/adacore-technologies-for-airborne-software/images/standards-fig2.png

20.1 KB
Loading

‎content/booklets/adacore-technologies-for-airborne-software/index.rst

Lines changed: 169 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,169 @@
1+
.. include:: ./common_defs.rst
2+
3+
:prev_state: False
4+
:next_state: False
5+
6+
.. _AdaCore_Technologies_Airborne_Software_Index:
7+
8+
AdaCore Technologies for Airborne Software
9+
==========================================
10+
11+
.. subtitle for outputs other than PDF that has it on front page
12+
.. only:: builder_html or builder_epub
13+
14+
Supporting certification and tool qualification for DO-178C:ED-12C
15+
16+
.. include:: ../../courses/global.txt
17+
18+
.. only:: no_hidden_books
19+
20+
.. meta::
21+
:robots: noindex, nofollow
22+
23+
.. warning::
24+
25+
This version of the website contains UNPUBLISHED contents.
26+
27+
.. only:: builder_epub
28+
29+
Release |release|
30+
31+
|today|
32+
33+
.. only:: builder_latex or builder_epub
34+
35+
.. container:: content-copyright
36+
37+
Copyright © 2017 |ndash| 2025, AdaCore
38+
39+
This book is published under a CC BY-SA license, which means that you
40+
can copy, redistribute, remix, transform, and build upon the content
41+
for any purpose, even commercially, as long as you give appropriate
42+
credit, provide a link to the license, and indicate if changes were
43+
made. If you remix, transform, or build upon the material, you must
44+
distribute your contributions under the same license as the original.
45+
You can find license details
46+
`on this page <http://creativecommons.org/licenses/by-sa/4.0>`_
47+
48+
.. image:: ../../images/ccheart_black.png
49+
:width: 108pt
50+
51+
.. only:: builder_html
52+
53+
.. container:: ebook-download
54+
55+
.. raw:: html
56+
57+
<a class="ebook-download-button" href="/pdf_books/booklets/adacore-technologies-for-airborn-software.pdf">
58+
Download PDF
59+
</a>
60+
61+
<a class="ebook-download-button" href="/epub_books/booklets/adacore-technologies-for-airborn-software.epub">
62+
Download EPUB
63+
</a>
64+
65+
.. only:: builder_latex or builder_epub
66+
67+
.. raw:: latex
68+
69+
\clearpage
70+
71+
.. rubric:: **About the Authors**
72+
73+
Frédéric Pothon
74+
75+
During his professional career dating back to the 1980s,
76+
Frédéric Pothon has been a recognized expert in the area of
77+
software aspects of certification (most notably |do-178|,
78+
Levels A, B, and C). He was a member of the EUROCAE/RTCA
79+
group that produced |do-248b|, which provides supporting
80+
information for the |do-178b| standard. Mr. Pothon has
81+
led projects at Turboméca (now Safran Helicopter Engines)
82+
and Airbus, where he was responsible for software methodologies
83+
and quality engineering processes. He founded the company
84+
ACG-Solutions in 2007 and worked as an independent consulting
85+
engineer, providing training, audits, and support, and he was
86+
involved in several research projects. Mr. Pothon
87+
is an expert in the qualification and utilization of automatic
88+
code generation tools for model-based development, and he
89+
served as co-chair of the Tool Qualification subgroup during
90+
the |do-178c| project.
91+
92+
Quentin Ochem
93+
94+
Quentin Ochem is the Chief Product and Revenue Officer at AdaCore,
95+
where he oversees marketing, sales, and product management while
96+
steering the company's strategic initiatives. He joined
97+
AdaCore in 2005 to work on the company's Integrated Development
98+
Environments and cross-language bindings.
99+
With an extensive background in software engineering in high-integrity
100+
domains such as avionics and defense, he has served leading roles in technical
101+
sales, customer training, and product development. Notably, he has
102+
conducted training on the Ada language, AdaCore tools, and the
103+
|do-178b| and |do-178c| software certification standards. In 2021
104+
he stepped into his current role, directing the company's strategic
105+
initiatives.
106+
107+
.. rubric:: **Foreword**
108+
109+
The guidance in the |do-178c| standard and its associated
110+
technology-specific supplements helps achieve confidence that airborne
111+
software meets its requirements. Certifying that a system complies with
112+
this guidance is a challenging task, especially for the verification
113+
activities, but appropriate usage of qualified tools and specialized run-time
114+
libraries can significantly simplify the effort. This document explains
115+
how a number of technologies offered by AdaCore --- tools, libraries, and
116+
supplemental services --- can help. It covers not only the "core" |do-178c|
117+
standard but also the technology supplements: Object-Oriented
118+
Technology and Related Techniques |do-332|, and Formal
119+
Methods (|do-333|). The content is based on the authors' many
120+
years of practical experience with the certification of airborne software,
121+
with the Ada and SPARK programming languages, and with the
122+
technologies addressed by the |do-178c| supplements.
123+
124+
We gratefully acknowledge the assistance of Ben Brosgol
125+
(AdaCore) for his review of and contributions to the material presented in
126+
this document.
127+
128+
| Frédéric Pothon, ACG Solutions
129+
| Montpellier, France
130+
| March 2017
131+
132+
| Quentin Ochem, AdaCore
133+
| New York, NY
134+
| March 2017
135+
136+
.. rubric:: Foreword to V2.1
137+
138+
This revised booklet reflects the evolution of and enhancements to
139+
AdaCore's products since the earlier edition.
140+
Among other updates, the static analysis tools supplementing the
141+
GNAT Pro development environment have been integrated
142+
into a cohesive toolset (the *GNAT Static Analysis Suite*).
143+
The dynamic analysis tools have likewise been consolidated, and
144+
the resulting *GNAT Dynamic Analysis Suite* has introduced
145+
a fuzzing tool --- *GNATfuzz* --- which exercises the software
146+
with invalid input and checks for failsafe behavior.
147+
148+
I would like to express my appreciation to Olivier Appere (AdaCore) for
149+
his detailed and helpful review of the content for the revised booklet.
150+
151+
| Ben Brosgol, AdaCore
152+
| Bedford, Massachusetts
153+
| July 2025
154+
155+
156+
.. toctree::
157+
:maxdepth: 4
158+
:numbered:
159+
160+
Introduction<introduction>
161+
The DO-178C/ED-12C Standards Suite<standards>
162+
AdaCore Tools and Technologies Overview<tools>
163+
Compliance with DO-178C / ED-12C Guidance: Analysis<analysis>
164+
Summary of contributions to DO-178C/ED-12C objectives<summary>
165+
166+
.. toctree::
167+
:maxdepth: 2
168+
169+
References<references>

‎content/booklets/adacore-technologies-for-airborne-software/introduction.rst

Lines changed: 87 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,87 @@
1+
.. include:: common_defs.rst
2+
3+
Introduction
4+
============
5+
6+
This document explains how to use AdaCore's technologies --- the company's tools,
7+
run-time libraries, and associated services --- in conjunction with the
8+
safety-related standards for airborne software: |do-178c| and
9+
and its technology supplements and tool qualification considerations. It
10+
describes how AdaCore's technologies fit into a project's software life
11+
cycle processes, and how they can satisfy various objectives of the standards.
12+
Many of the advantages of AdaCore's products stem from the software
13+
engineering support found in the Ada programming language, including
14+
features (such as contract-based programming) introduced in Ada\ |nbsp|\ 2012 [ISO_IEC_2012]_.
15+
Other advantages draw directly from the formally analyzable SPARK subset
16+
of Ada [AdaCore_Altran_2020]_, [Dross_2022]_, [Chapman_et_al_2024]_.
17+
As a result, this document identifies how Ada and SPARK contribute toward the development
18+
of reliable software. AdaCore personnel have played key roles in the
19+
design and implementation of both of these languages.
20+
21+
.. index:: V software life cycle
22+
23+
Although |do-178c| doesn't prescribe any specific software life cycle, the
24+
development and verification processes that it encompasses can be represented
25+
as a variation of the traditional "V" cycle. As shown in :numref:`fig1`, AdaCore's
26+
products and the Ada and SPARK languages contribute principally to the bottom
27+
portions of the "V" --- coding and integration and their verification. The Table
28+
annotations in :numref:`fig1` refer to the tables in |do-178c| and, when
29+
applicable, specific objectives in those tables.
30+
31+
.. _fig1:
32+
.. figure:: images/introduction-fig1.png
33+
:align: center
34+
35+
AdaCore Technologies and |do-178c| Life Cycle Processes
36+
37+
Complementing AdaCore's support for Ada and SPARK, the company offers tools and technologies for C, C++ and Rust.
38+
Although C lacks the built-in checks as well as other
39+
functionality that Ada provides, AdaCore's Ada and C toolchains have similar capabilities. And mixed-language applications can take
40+
advantage of Ada's interface checking that is performed during inter-module communication.
41+
42+
AdaCore's Ada and C compilers can help developers produce reliable software, targeting embedded platforms with RTOSes as well as
43+
"bare metal" configurations. These are available with long term support, certifiable run-time libraries, and source-to-object
44+
traceability analyses as required for |do-178c| Level A. Supplementing the compilers are a comprehensive set of static
45+
and dynamic analysis tools, including a code standard enforcer, a vulnerability and logic error detector, test and coverage analyzers,
46+
and a fuzzing tool.
47+
48+
.. index:: Tool qualification
49+
50+
A number of these tools are qualifiable with respect to the |do-330| standard (Tool Qualification Considerations).
51+
The use of qualified tools can save considerable effort during development and/or verification since the output of the tools does not
52+
need to be manually checked. Qualification material, at the applicable Tool Qualification Level (TQL), is available for specific
53+
AdaCore tools.
54+
55+
Supplementing the core |do-178c| standard are three supplements that address specific technologies:
56+
57+
.. index:: DO-331/ED-218: Model-Based Development and Verification
58+
59+
* *DO-331/ED-218: Model-Based Development and Verification*
60+
61+
AdaCore's tools and technologies can be used in conjunction with model-based methods but do not relate
62+
directly to the issues addressed in |do-331|.
63+
64+
.. index:: DO-332/ED-217: Object-Oriented Technology and Related Techniques
65+
66+
* *DO-332/ED-217: Object-Oriented Technology and Related Techniques*
67+
68+
The Ada and SPARK languages provide specific features that help meet the objectives of |do-332|,
69+
thus allowing developers to exploit Object Orientation (e.g., class hierarchies and inheritance for
70+
specifying data relationships) in a certified application.
71+
72+
.. index:: DO-333/ED-216: Formal Methods
73+
.. index:: SPARK language
74+
75+
* *DO-333/ED-216: Formal Methods*
76+
77+
The SPARK language and toolset directly support |do-333|, allowing the use of formal proofs
78+
to replace some low-level testing.
79+
80+
The technologies and associated options presented in this document are known to be acceptable, and certification authorities have
81+
already accepted most of them on actual projects. However, acceptance is project dependent. An activity using a technique or method
82+
may be considered as appropriate to satisfy one or several |do-178c| objectives for one project (determined by the development
83+
standards, the input complexity, the target computer and system environment) but not necessarily on another project. The effort and
84+
amount of justification to gain approval may also differ from one auditor to another, depending of their background. Whenever a new
85+
tool, method, or technique is introduced, it's important to open a discussion with AdaCore and the designated authority to confirm
86+
its acceptability. The level of detail in the process description provided in the project plans and standard is a key factor in
87+
gaining acceptance.

‎content/booklets/adacore-technologies-for-airborne-software/references.rst

Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
.. only:: builder_html or builder_epub
2+
3+
.. rubric:: References
4+
5+
References
6+
==========
7+
8+
9+
.. [AdaCore_2016] AdaCore; *High-Integrity Object-Oriented Programming in Ada*, Version 1.4, October 2016.
10+
Available at https://www.adacore.com/knowledge/technical-papers/high-integrity-oop-in-ada/
11+
12+
.. [AdaCore_Altran_2020] AdaCore and Altran; *SPARK Reference Manual, Release 2020*,
13+
Available at https://www.adacore.com/uploads/techPapers/spark_rm_community_2020.pdf
14+
15+
.. [AdaCore_Thales_2020] AdaCore and Thales; *Implementation Guidance for the Adoption of SPARK*, Release 1.2; July 2020.
16+
Available at https://www.adacore.com/books/implementation-guidance-spark
17+
18+
.. [AdaLearn] AdaCore; Online training for Ada and SPARK. Available at https://learn.adacore.com/
19+
20+
.. [Barnes_2014] John Barnes; *Programming in Ada 2012*, Cambridge University Press, 2014.
21+
22+
.. [Barnes_Brosgol_2015] John Barnes and Ben Brosgol; *Safe and Secure Software, an invitation to Ada 2012*, AdaCore, 2015.
23+
Available at https://www.adacore.com/books/safe-and-secure-software
24+
25+
.. [Black_et_al_2011] Paul E. Black, Michael Kass, Michael Koo, Elizabeth Fong; *Source Code Security Analysis Tool Functional Specification*,
26+
National Institute for Standards and Technology (NIST), 2011.
27+
28+
.. [CCDB_2022] Common Criteria Development Board; *Common Criteria for Information Technology Security Evaluation (ISO/IEC 15408)*, 2022.
29+
See https://www.commoncriteriaportal.org/
30+
31+
.. [Chapman_et_al_2024] Roderick Chapman, Claire Dross, Stuart Matthews, and Yannick Moy; "Co-Developing Programs and Their Proof of Correctness",
32+
in *Communications of the ACM*, Vol. 67, No. 3, March 2024.
33+
Available at https://www.adacore.com/uploads/techPapers/Co-Developing-Programs-and-Their-Proof-of-Correctness.pdf
34+
35+
.. [Dross_2022] Claire Dross; "The Work of Proof in SPARK", in *Ada User Journal* Vol. 35, No. 1, September 2022.
36+
Available at https://www.adacore.com/uploads/techPapers/222293-adacore-spark-press-paper-v3.pdf
37+
38+
.. [Hayhurst_et_al_2001] Kelly J. Hayhurst, Dan S. Veerhusen, John J. Chilenski, Leanna K. Rierson; *A Practical Tutorial on Modified Condition / Decision Coverage*;
39+
NASA / TM-2001-210876; May 2001.
40+
Available at https://shemesh.larc.nasa.gov/fm/papers/Hayhurst-2001-tm210876-MCDC.pdf
41+
42+
.. [ICAO_1944] ICAO, *Convention on International Civil Aviation*; December 1944. Available at https://www.icao.int/publications/documents/7300_orig.pdf
43+
44+
.. [ISO_IEC_2012] ISO/IEC; *Ada Language Reference Manual, Language and Standard Libraries*, 2012.
45+
Available at https://www.adaic.org/ada-resources/standards/ada12/
46+
47+
.. [ISO_IEC_2022] ISO/IEC; *Ada Reference Manual, Language and Standard Libraries*, 2022.
48+
Available at https://www.adaic.org/ada-resources/standards/ada22/
49+
50+
.. [Kanig_Ochem_Comar_2016] Johannes Kanig, Quentin Ochem, Cyrille Comar; *Bringing SPARK to C developers*, ERTS, 2016.
51+
52+
.. [McCormick_Chapin_2015] John W. McCormick and Peter C. Chapin; *Building High Integrity Applications with SPARK*, Cambridge University Press, 2015.
53+
54+
.. [Moy_et_al_2013] Yannick Moy, Emmanuel Ledinot, Hervé Delseny, Virginie Wiels, Benjamin Monate; "Testing or Formal Verification: DO-178C Alternatives and Industrial Experience",
55+
*IEEE Software*, 2013.
56+
57+
.. [Moy_2017] Yannick Moy; "Formal program verification in avionics certification", *Military Embedded Systems*, February 24, 2017.
58+
Available at https://militaryembedded.com/avionics/safety-certification/formal-program-verification-avionics-certification
59+
60+
.. [Rierson_2013] Leanna Rierson, *Developing Safety-Critical Software: A Practical Guide for Aviation Software and DO-178C Compliance*, CRC Press, 2013.
61+
62+
.. [RTCA_EUROCAE_2011] *Software Considerations in Airborne Systems and Equipment Certification* (RTCA DO-178C / EUROCAE ED-12C), December 2011;
63+
Available for a fee at https://my.rtca.org/productdetails?id=a1B36000001IcmqEAC and https://eshop.eurocae.net/eurocae-documents-and-reports/ed-12c-with-corrigendum-1/#
64+
65+
.. Uncited reference
66+
Matteo Bordin, Cyrille Comar, Tristan Gingold, Jérôme Guitton, Olivier Hainque,
67+
Thomas Quinot, *Object and Source Coverage for Critical Applications with the COUVERTURE Open Analysis Framework*, ERTS, 2010.

0 commit comments

Comments
 (0)