First version of the Airborne Software Booklet

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

@@ -0,0 +1,6 @@
+.. only:: builder_html or builder_epub
+
+	  Bibliography
+	  ============
+
+.. bibliography::

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

@@ -0,0 +1,5 @@
+[DEFAULT]
+title=AdaCore Technologies for Airborne Software
+author=Frédéric Pothon \\and Quentin Ochem
+version=2.1
+bibtex_file=references.bib

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

@@ -0,0 +1,163 @@
+.. include:: ../../courses/global.txt
+
+:prev_state: False
+:next_state: False
+
+.. _AdaCore_Technologies_Airborne_Software_Index:
+
+AdaCore Technologies for Airborne Software
+==========================================
+
+.. subtitle for outputs other than PDF that has it on front page
+.. only:: builder_html or builder_epub
+
+	  Supporting certification and tool qualification for DO-178C:ED-12C
+
+.. include:: ../../courses/global.txt
+
+.. only:: no_hidden_books
+
+    .. meta::
+        :robots: noindex, nofollow
+
+    .. warning::
+
+        This version of the website contains UNPUBLISHED contents.
+
+.. only:: builder_epub
+
+    Release |release|
+
+    |today|
+
+.. only:: builder_latex or builder_epub
+
+    .. container:: content-copyright
+
+        Copyright © 2017 |ndash| 2025, AdaCore
+
+        This book is published under a CC BY-SA license, which means that you
+        can copy, redistribute, remix, transform, and build upon the content
+        for any purpose, even commercially, as long as you give appropriate
+        credit, provide a link to the license, and indicate if changes were
+        made. If you remix, transform, or build upon the material, you must
+        distribute your contributions under the same license as the original.
+        You can find license details
+        `on this page <http://creativecommons.org/licenses/by-sa/4.0>`_
+
+        .. image:: ../../images/ccheart_black.png
+            :width: 108pt
+
+.. only:: builder_html
+
+    .. container:: ebook-download
+
+        .. raw:: html
+
+            <a class="ebook-download-button" href="/pdf_books/booklets/adacore-technologies-for-airborn-software.pdf">
+                Download PDF
+            </a>
+
+            <a class="ebook-download-button" href="/epub_books/booklets/adacore-technologies-for-airborn-software.epub">
+                Download EPUB
+            </a>
+
+.. only:: builder_latex or builder_epub
+
+    .. raw:: latex
+
+        \clearpage
+
+.. rubric:: **About the Authors**
+
+Frédéric Pothon
+
+During his professional career dating back to the 1980s, Frédéric
+Pothon has been a recognized expert in the area of software aspects of
+certification (most notably |do-178|, Levels A, B, and C). He was a
+member of the EUROCAE/RTCA group that produced |do-248b|, which
+provides supporting information for the |do-178b| standard. Mr. Pothon
+has led projects at Turboméca (now Safran Helicopter Engines) and
+Airbus, where he was responsible for software methodologies and
+quality engineering processes. He founded the company ACG-Solutions in
+2007 and worked as an independent consulting engineer, providing
+training, audits, and support, and he was involved in several research
+projects. Mr. Pothon is an expert in the qualification and utilization
+of automatic code generation tools for model-based development, and he
+served as co-chair of the Tool Qualification subgroup during the
+|do-178c| project.
+
+Quentin Ochem
+
+Quentin Ochem is the Chief Product and Revenue Officer at AdaCore,
+where he oversees marketing, sales, and product management while
+steering the company's strategic initiatives. He joined AdaCore in
+2005 to work on the company's Integrated Development Environments and
+cross-language bindings.  With an extensive background in software
+engineering in high-integrity domains such as avionics and defense, he
+has served leading roles in technical sales, customer training, and
+product development. Notably, he has conducted training on the Ada
+language, AdaCore tools, and the |do-178b| and |do-178c| software
+certification standards. In 2021 he stepped into his current role,
+directing the company's strategic initiatives.
+
+.. rubric:: **Foreword**
+
+The guidance in the |do-178c| standard and its associated
+technology-specific supplements helps achieve confidence that airborne
+software meets its requirements. Certifying that a system complies
+with this guidance is a challenging task, especially for the
+verification activities, but appropriate usage of qualified tools and
+specialized run-time libraries can significantly simplify the
+effort. This document explains how a number of technologies offered by
+AdaCore |mdash| tools, libraries, and supplemental services |mdash|
+can help. It covers not only the "core" |do-178c| standard but also
+the technology supplements: Object-Oriented Technology and Related
+Techniques |do-332|, and Formal Methods (|do-333|). 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 the technologies addressed by the |do-178c|
+supplements.
+
+We gratefully acknowledge the assistance of Ben Brosgol (AdaCore) for
+his review of and contributions to the material presented in this
+document.
+
+| Frédéric Pothon, ACG Solutions
+| Montpellier, France
+| March 2017
+
+| Quentin Ochem, AdaCore
+| New York, NY
+| March 2017
+
+.. rubric:: Foreword to V2.1
+
+This revised booklet reflects the evolution of and enhancements to
+AdaCore's products since the earlier edition.  Among other updates,
+the static analysis tools supplementing the GNAT Pro development
+environment have been integrated into a cohesive toolset (the *GNAT
+Static Analysis Suite*).  The dynamic analysis tools have likewise
+been consolidated, and the resulting *GNAT Dynamic Analysis Suite* has
+introduced a fuzzing tool |mdash| *GNATfuzz* |mdash| which exercises
+the software with invalid input and checks for failsafe behavior.
+
+I would like to express my appreciation to Olivier Appere (AdaCore)
+for his detailed and helpful review of the content for the revised
+booklet.
+
+| Ben Brosgol, AdaCore
+| Bedford, Massachusetts
+| July 2025
+
+
+.. toctree::
+   :maxdepth: 4
+   :numbered:    
+
+   Introduction<introduction>
+   The DO-178C/ED-12C Standards Suite<standards>
+   AdaCore Tools and Technologies Overview<tools>
+   Compliance with DO-178C / ED-12C Guidance: Analysis<analysis>
+   Summary of contributions to DO-178C/ED-12C objectives<summary>
+   Bibliography<bibliography>

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

@@ -0,0 +1,107 @@
+.. include:: ../../courses/global.txt
+
+Introduction
+============
+
+This document explains how to use AdaCore's technologies |mdash| the
+company's tools, run-time libraries, and associated services |mdash|
+in conjunction with the safety-related standards for airborne
+software: |do-178c| and 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 software engineering support found
+in the Ada programming language, including features (such as
+contract-based programming) introduced in Ada\ |nbsp|\ 2012
+:cite:p:`ISO_IEC_2012`.  Other advantages draw directly from the
+formally analyzable SPARK subset of Ada :cite:p:`AdaCore_Altran_2020`,
+:cite:p:`Dross_2022`, :cite:p:`Chapman_et_al_2024`.  As a result, this
+document identifies how Ada and SPARK contribute toward the
+development of reliable software. AdaCore personnel have played key
+roles in the design and implementation of both of these languages.
+
+.. index:: V software life cycle
+
+Although |do-178c| doesn't prescribe any specific software life cycle,
+the development and verification processes that it encompasses can be
+represented as a variation of the traditional
+:wikipedia:`"V-model"<V-model_(software_development)>`. As shown in
+:numref:`Airborn_SW_fig1`, AdaCore's products and the Ada and SPARK
+languages contribute principally to the bottom portions of the "V"
+|mdash| coding and integration and their verification. The Table
+annotations in :numref:`Airborn_SW_fig1` refer to the tables in
+|do-178c| and, when applicable, specific objectives in those tables.
+
+.. _Airborn_SW_fig1:
+.. figure:: images/introduction-fig1.png
+   :align: center
+
+   AdaCore Technologies and |do-178c| Life Cycle Processes
+
+Complementing AdaCore's support for Ada and SPARK, the company offers
+tools and technologies for C, C++ and Rust.  Although C lacks the
+built-in checks as well as other functionality that Ada provides,
+AdaCore's Ada and C toolchains have similar capabilities. And
+mixed-language applications can take advantage of Ada's interface
+checking that is performed during inter-module communication.
+
+AdaCore's Ada and C compilers can help developers produce reliable
+software, targeting embedded platforms with RTOSes as well as "bare
+metal" configurations. These are available with long term support,
+certifiable run-time libraries, and source-to-object traceability
+analyses as required for |do-178c| Level A. Supplementing the
+compilers are a comprehensive set of static and dynamic analysis
+tools, including a code standard enforcer, a vulnerability and logic
+error detector, test and coverage analyzers, and a fuzzing tool.
+
+.. index:: Tool qualification
+
+A number of these tools are qualifiable with respect to the |do-330|
+standard (Tool Qualification Considerations).  The use of qualified
+tools can save considerable effort during development and/or
+verification since the output of the tools does not need to be
+manually checked. Qualification material, at the applicable Tool
+Qualification Level (TQL), is available for specific AdaCore tools.
+
+Supplementing the core |do-178c| standard are three supplements that
+address specific technologies:
+
+.. index:: DO-331/ED-218: Model-Based Development and Verification
+
+* *DO-331/ED-218: Model-Based Development and Verification*
+
+  AdaCore's tools and technologies can be used in conjunction with
+  model-based methods but do not relate directly to the issues
+  addressed in |do-331|.
+
+.. index:: DO-332/ED-217: Object-Oriented Technology and Related Techniques
+
+* *DO-332/ED-217: Object-Oriented Technology and Related Techniques*
+
+  The Ada and SPARK languages provide specific features that help meet
+  the objectives of |do-332|, thus allowing developers to exploit
+  Object Orientation (e.g., class hierarchies and inheritance for
+  specifying data relationships) in a certified application.
+
+.. index:: DO-333/ED-216: Formal Methods
+.. index:: SPARK language
+
+* *DO-333/ED-216: Formal Methods*
+
+  The SPARK language and toolset directly support |do-333|, allowing
+  the use of formal proofs to replace some low-level testing.
+
+The technologies and associated options presented in this document are
+known to be acceptable, and certification authorities have already
+accepted 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|
+objectives for one project (determined by the development standards,
+the input complexity, the target computer and system environment) but
+not necessarily 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 is introduced, it's important to open a discussion with
+AdaCore and the designated authority to confirm its acceptability. The
+level of detail in the process description provided in the project
+plans and standard is a key factor in gaining acceptance.