Skip to content

Commit b061d8e

Browse files
gusthoffgusthoff
authored
Merge pull request #1252 from AdaCore/airborne-software-booklet
First version of the Airborne Software Booklet
2 parents 5f134e0 + 6b21974 commit b061d8e

File tree

16 files changed

+6296
-1
lines changed

16 files changed

+6296
-1
lines changed

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

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

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

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
.. only:: builder_html or builder_epub
2+
3+
Bibliography
4+
============
5+
6+
.. bibliography::

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

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

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

Lines changed: 272 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,272 @@
1+
.. include:: ../../../global.txt
2+
3+
.. index:: DO-178C/ED-12C
4+
5+
The DO-178C/ED-12C Standards Suite
6+
==================================
7+
8+
Overview
9+
---------
10+
11+
"Every State has complete and exclusive sovereignty over the airspace
12+
above its territory." This general principle was codified in Article 1
13+
of the Convention on International Civil Aviation (the "Chicago
14+
Convention") in 1944 :cite:p:`ICAO_1944`. To control the airspace,
15+
harmonized regulations have been formulated to ensure that the
16+
aircraft are airworthy.
17+
18+
A type certificate is issued by a certification authority to signify
19+
the airworthiness of an aircraft manufacturing design. The certificate
20+
reflects a determination made by the regulating body that the aircraft
21+
is manufactured according to an approved design, and that the design
22+
complies with airworthiness requirements. To meet those requirements
23+
the aircraft and each subassembly must also be approved. Typically,
24+
requirements established by a regulating body refer to "Minimum
25+
Operating Performance Standards" (MOPS) and a set of recognized
26+
"Acceptable Means of Compliance" such as |do-178| for software,
27+
|do-160| for environmental conditions and test procedures, and
28+
|do-254| for Complex Electronic Hardware.
29+
30+
*DO-178C/ED-12C - Software Considerations in Airborne Systems and
31+
Equipment Certification* :cite:p:`RTCA_EUROCAE_2011` |mdash| was issued in
32+
December 2011, developed jointly by RTCA, Inc., and EUROCAE. It is the
33+
primary document by which certification authorities such as the FAA,
34+
EASA, and Transport Canada approve all commercial software-based
35+
aerospace systems.
36+
37+
The |do-178c| document suite comprises:
38+
39+
* The core document, which is a revision of the previous release
40+
(|do-178b|). The changes are mostly clarifications, and also
41+
address the use of "Parameter Data Items" (e.g., Configuration
42+
tables)
43+
44+
.. index:: DO-278A/ED-109A: Software Integrity Assurance
45+
Considerations for CNS/ATM Systems
46+
47+
* |do-278a|, which is similar to |do-178c| and addresses ground-based
48+
software used in the domain of CNS/ATM (Communication Navigation
49+
Surveillance/Air Traffic Management)
50+
51+
.. index:: DO-248C/ED-94C: Supporting Information for DO-178C/ED-12C
52+
and DO-278A/ED-109A
53+
54+
* |do-248c| (Supporting Information for |do-178c| and |do-278a|),
55+
which explains the rationale behind the guidance provided in the
56+
core documents
57+
58+
.. index:: DO-331/ED-218: Model-Based Development and Verification
59+
.. index:: DO-332/ED-217: Object-Oriented Technology and Related
60+
Techniques
61+
.. index:: DO-333/ED-216: Formal Methods
62+
63+
* Three technology-specific supplements
64+
65+
* |do-331|: Model-Based Development and Verification
66+
* |do-332|: Object Oriented Technology and Related Techniques
67+
* |do-333|: Formal Methods
68+
69+
Each supplement adapts the core document guidance as appropriate for
70+
its respective technology. These supplements are not standalone
71+
documents but must be used in conjunction with |do-178c| or
72+
|do-278a|.
73+
74+
.. index:: DO-330/ED-215: Software Tool Qualification Considerations
75+
76+
* |do-330| (Software Tool Qualification Considerations), providing
77+
guidance for qualifying software tools. This standard is not
78+
specific to |do-178c| and may be applied to software certification
79+
in other application domains.
80+
81+
Details on how to use these standards in practice may be found in
82+
:cite:p:`Rierson_2013`.
83+
84+
.. index:: Design Assurance Level (DAL), Software level
85+
86+
One of the main principles of the |do-178c| document suite is to be
87+
"objective oriented". The guidance in each document consists of a set
88+
of objectives that relate to the various software life-cycle processes
89+
(planning, development, verification, configuration management,
90+
quality assurance, certification liaison). The objectives that must be
91+
met for a particular software component depend on the software level
92+
(also known as a *Design Assurance Level* or *DAL*) of the
93+
component. The level in turn is based on the potential effect of an
94+
anomaly in that software component on the continued safe operation of
95+
the aircraft. Software levels range from `E` (the lowest) where there
96+
is no effect, to `A` (the highest) where an anomaly can cause the loss
97+
of the aircraft. A software component's level is established as part
98+
of the system life-cycle processes.
99+
100+
To gain software approval for a system, the applicant has to
101+
demonstrate that the objectives relevant to the software level for
102+
each component have been met. To achieve this goal, the development
103+
team specifies the various software life-cycle activities (based on
104+
those recommended by |do-178c| and/or others), and its associated
105+
methods, environment, and organization/management. In case the chosen
106+
methods are addressed by one of the technology supplements, additional
107+
or alternative objectives must also be satisfied. The technology
108+
supplements may replace or add objectives and/or activities.
109+
110+
.. index:: DO-330/ED-215: Software Tool Qualification Considerations
111+
112+
Software Tool Qualification Considerations: DO-330/ED-215
113+
-------------------------------------------------------------
114+
115+
A software tool needs to be qualified when a process is automated,
116+
eliminated, or reduced, but its outputs are not verified. The
117+
systematic verification of the tool outputs is replaced by activities
118+
performed on the tool itself: the "tool qualification". The
119+
qualification effort depends on the assurance level of the airborne
120+
software and the possible effect that an error in the tool may have on
121+
this software. The resulting combination, the Tool Qualification
122+
Level, is a 5 level scale, from TQL-5 (the lowest level, applicable to
123+
software tools that cannot insert an error in the resulting software,
124+
but might fail to detect an error) to TQL-1 (the highest, applicable
125+
to software tools that can insert an error in software at level A).
126+
127+
A tool is only qualified in the context of a specific project, for a
128+
specific certification credit, expressed in term of objectives and
129+
activities. Achieving qualification for a tool on a specific project
130+
does of course greatly increase the likelihood of being able to
131+
qualify the tool on another project. However, a different project may
132+
have different processes or requirements, or develop software with
133+
different environment constraints. As a result, the qualifiability of
134+
a tool needs to be systematically assessed on a case-by-case basis.
135+
136+
Although many references are made in the literature about "qualified"
137+
tools, strictly speaking this term should only be used in the context
138+
of a specific project. Tools provided by tool vendors, independently
139+
of any project, should be identified as "qualifiable" only. The tool
140+
qualification document guidance |do-330| includes specific objectives
141+
that can only be satisfied in the context of a given project
142+
environment.
143+
144+
Throughout this document, the applicable tool qualification level is
145+
identified together with the relevant objective or activity for which
146+
credit may be sought. The qualification activities have been performed
147+
with respect to |do-330| at the applicable Tool Qualification
148+
Level. Tool qualification material is available to customers as a
149+
supplement to AdaCore's GNAT Pro Assurance product.
150+
151+
.. index:: DO-331/ED-218: Model-Based Development and Verification
152+
153+
Model-Based Development and Verification Supplement: DO-331/ED-218
154+
--------------------------------------------------------------------
155+
156+
Model-based development covers a wide range of techniques for
157+
representing the software requirements and/or architecture, most often
158+
through a graphical notation. The source code itself is not
159+
considered as a model. Well known examples include UML for software
160+
architecture, SysSML for system representation, and Simulink\ |copy|
161+
for control algorithms and related requirements. |do-331| presents the
162+
objectives and activities associated with the use of such techniques.
163+
164+
The main added value of the supplement is its guidance on how to use
165+
model simulation and obtain certification credit. AdaCore's tools and
166+
technologies can be used in conjunction with model-based methods but
167+
do not relate directly to the issues addressed in this supplement.
168+
169+
.. index:: DO-332/ED-217: Object-Oriented Technology and Related
170+
Techniques
171+
172+
Object-Oriented Technology and Related Techniques Supplement: DO-332/ED-217
173+
------------------------------------------------------------------------------
174+
175+
Although |do-332| is often referred as the "object oriented
176+
supplement", the "related techniques" mentioned in the title are
177+
equally relevant and are addressed in detail. They may be used in
178+
conjunction with Object-Oriented Technology (OOT) but are not
179+
necessarily related to OO features. Such "related techniques" include
180+
virtualization, genericity (also known as templates), exceptions,
181+
overloading, and dynamic memory management.
182+
183+
Considering the breadth of features covered by |do-332|, at least some
184+
of its guidance should be followed regardless of whether the actual
185+
application is using object orientation. For example, type conversion
186+
is probably present in most code bases regardless of which language is
187+
being used.
188+
189+
The |do-332| supplement is much more code-centric than the others, and
190+
only two objectives are added: one related to local type consistency
191+
(dynamic dispatching) and another one related to dynamic memory. All
192+
other guidance takes the form of additional activities for existing
193+
|do-178c| objectives.
194+
195+
Of particular relevance is the supplement's *Vulnerability Analysis*
196+
annex. Although not binding, it explains in detail what is behind
197+
these additional activities. The following features in particular may
198+
need to be addressed when Ada is used:
199+
200+
* Inheritance / local type consistency
201+
* Parametric polymorphism (genericity)
202+
* Overloading
203+
* Type conversion
204+
* Exception management
205+
* Dynamic memory
206+
* Component-based development
207+
208+
The Ada language, the precautions taken during the design and coding
209+
processes, and the use of AdaCore tools combine to help address or
210+
mitigate the vulnerabilities associated with these features.
211+
212+
.. index:: DO-333/ED-216: Formal Methods
213+
214+
Formal Methods Supplement: DO-333/ED-216
215+
------------------------------------------
216+
217+
|do-333| provides guidance on the use of formal methods. A formal
218+
method is defined as "a formal model combined with a formal
219+
analysis". A formal model should be precise, unambiguous and have a
220+
mathematically defined syntax and semantics. The formal analysis
221+
should be sound; i.e., if it is supposed to determine whether the
222+
formal model (for example the software source code in a language such
223+
as SPARK) satisfies a given property, then the analysis should never
224+
assert that the property holds when in fact it does not.
225+
226+
A formal method may be used to satisfy |do-178c| verification
227+
objectives; formal analysis may therefore replace some reviews,
228+
analyses and tests. Almost all verification objectives are potential
229+
candidates for formal methods.
230+
231+
In |do-178c|, the purpose of testing is to verify the Executable
232+
Object Code (EOC) based on the requirements. The main innovation of
233+
DO-333 / ED-216 is to allow the use of formal methods to replace some
234+
categories of tests. In fact, with the exception of software /
235+
hardware integration tests showing that the EOC is compatible with the
236+
target computer, the other objectives of EOC verification may be
237+
satisfied by formal analysis. This is a significant added
238+
value. However, employing formal analysis to replace tests is a new
239+
concept in the avionics domain, with somewhat limited experience in
240+
practice thus far (see :cite:p:`Moy_et_al_2013` for further
241+
information). As noted in :cite:p:`Moy_2017`, a significant issue is
242+
how to demonstrate that the compiler generates code that properly
243+
preserves the properties that have been formally demonstrated for the
244+
source code. Running the integration tests both with and without the
245+
contracts being executed, and showing that the results are the same in
246+
both cases, is one way to gain the necessary confidence that
247+
properties have been preserved in the EOC.
248+
249+
Details from tool providers on the underlying models or mathematical
250+
theories implemented in the tool are necessary to assess the maturity
251+
of the method. Then substantiation and justification need to be
252+
documented, typically in the Plan for Software Aspects of
253+
Certification (PSAC), and provided to certification authorities at an
254+
early stage for review.
255+
256+
.. index:: single: SPARK language; Eliminating / reducing testing
257+
258+
AdaCore provides the SPARK technology as a formal method that can
259+
eliminate or reduce the testing based on low-level requirements.
260+
Using SPARK will also get full or partial credit for other objectives,
261+
such as requirements and code accuracy and consistency, verifiability,
262+
etc. Its usage is consistent with the example provided in Appendix B
263+
of |do-333|, "FM.B.1.5.1 Unit Proof", and a SPARK version of this
264+
example is shown in :ref:`Airborn_SW_SPARK_Development_Cycle_Example`.
265+
Certification credit for using formal proofs is summarized in
266+
:numref:`Airborn_SW_fig2`:
267+
268+
.. _Airborn_SW_fig2:
269+
.. figure:: ../images/standards-fig2.png
270+
:align: center
271+
272+
SPARK contributions to verification objectives

0 commit comments

Comments
 (0)