AdaCore Technologies for Airborne Software

Supporting certification and tool qualification for DO-178C:ED-12C

Download PDF Download EPUB

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/ED ‑ 12, Levels A, B, and C). He was a member of the EUROCAE/RTCA group that produced DO ‑ 248B/ED ‑ 94B, which provides supporting information for the DO ‑ 178B/ED ‑ 12B 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/ED ‑ 12C 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/ED ‑ 12B and DO ‑ 178C/ED ‑ 12C software certification standards. In 2021 he stepped into his current role, directing the company's strategic initiatives.

Foreword

The guidance in the DO ‑ 178C/ED ‑ 12C 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 — tools, libraries, and supplemental services — can help. It covers not only the "core" DO ‑ 178C/ED ‑ 12C standard but also the technology supplements: 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 the technologies addressed by the DO ‑ 178C/ED ‑ 12C 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

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 — GNATfuzz — 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

• 1. Introduction
• 2. The DO-178C/ED-12C Standards Suite
  • 2.1. Overview
  • 2.2. Software Tool Qualification Considerations: DO-330/ED-215
  • 2.3. Model-Based Development and Verification Supplement: DO-331/ED-218
  • 2.4. Object-Oriented Technology and Related Techniques Supplement: DO-332/ED-217
  • 2.5. Formal Methods Supplement: DO-333/ED-216
• 3. AdaCore Tools and Technologies Overview
  • 3.1. Ada
    • 3.1.1. Background
    • 3.1.2. Language Overview
  • 3.2. SPARK
    • 3.2.1. Flexibility
    • 3.2.2. Powerful Static Verification
    • 3.2.3. Ease of Adoption
    • 3.2.4. Reduced Cost and Improved Efficiency of Executable Object Code (EOC) verification
  • 3.3. GNAT Pro Assurance
    • 3.3.1. Sustained Branches
    • 3.3.2. Configurable Run-Time Libraries
    • 3.3.3. Full Implementation of Ada Standards
    • 3.3.4. Source to Object Traceability
    • 3.3.5. Safety-Critical Support and Expertise
    • 3.3.6. Libadalang
    • 3.3.7. GNATstack
  • 3.4. GNAT Static Analysis Suite (GNAT SAS)
    • 3.4.1. Defects and vulnerability analysis
    • 3.4.2. GNATmetric
    • 3.4.3. GNATcheck
  • 3.5. GNAT Dynamic Analysis Suite (GNAT DAS)
    • 3.5.1. GNATtest
    • 3.5.2. GNATemulator
    • 3.5.3. GNATcoverage
    • 3.5.4. GNATfuzz
    • 3.5.5. TGen
  • 3.6. GNAT Pro for Rust
  • 3.7. Integrated Development Environments (IDEs)
    • 3.7.1. GNAT Studio
      • 3.7.1.1. Tools
      • 3.7.1.2. Robust, Flexible and Extensible
      • 3.7.1.3. Easy to learn, easy to use
      • 3.7.1.4. Remote Programming
    • 3.7.2. VS Code Extensions for Ada and SPARK
    • 3.7.3. Eclipse support - GNATbench
    • 3.7.4. GNATdashboard
• 4. Compliance with DO-178C / ED-12C Guidance: Analysis
  • 4.1. Overview
  • 4.2. Use case #1a: Coding with Ada 2012
    • 4.2.1. Benefits of the Ada language
      • 4.2.1.1. Modularization
      • 4.2.1.2. Strong typing
      • 4.2.1.3. Dimensionality checking
      • 4.2.1.4. Pointers
      • 4.2.1.5. Arrays
      • 4.2.1.6. Other Ada features
    • 4.2.2. Using Ada during the design process
      • 4.2.2.1. Component identification
      • 4.2.2.2. Low-Level Requirements
      • 4.2.2.3. Implementation of Hardware / Software Interfaces
    • 4.2.3. Integration of C components with Ada
    • 4.2.4. Robustness / defensive programming
    • 4.2.5. Defining and Verifying a Code Standard with GNATcheck
    • 4.2.6. Checking source code accuracy and consistency with GNAT SAS
    • 4.2.7. Checking worst case stack consumption with GNATstack
    • 4.2.8. Compiling with the GNAT Pro compiler
    • 4.2.9. Using GNATtest for low-level testing
      • 4.2.9.1. Approach 1: Test cases are not specified in Ada specifications
      • 4.2.9.2. Approach 2: Test cases are developed during the design process
      • 4.2.9.3. Approach 3: Test cases are developed separately from the design process
    • 4.2.10. Using GNATemulator for low-level and software / software integration tests
    • 4.2.11. Structural code coverage with GNATcoverage
    • 4.2.12. Data and control coupling coverage with GNATcoverage
    • 4.2.13. Demonstrating traceability of source to object code
  • 4.3. Use case #1b: Coding with Ada using OOT features
    • 4.3.1. Object orientation for the architecture
    • 4.3.2. Coverage in the case of generics
    • 4.3.3. Dealing with dynamic dispatching and substitutability
      • 4.3.3.1. Understanding Substitutability
      • 4.3.3.2. Verifying substitutability by pessimistic testing
      • 4.3.3.3. Verifying substitutability through requirement-based testing
      • 4.3.3.4. Verifying substitutability through formal proof
      • 4.3.3.5. Differences between local and global substitutability
    • 4.3.4. Dispatching as a new module coupling mechanism
    • 4.3.5. Memory management issues
    • 4.3.6. Exception handling
    • 4.3.7. Overloading and type conversion vulnerabilities
    • 4.3.8. Accounting for dispatching in performing resource analysis
  • 4.4. Use case #2: Using SPARK and Formal Methods
    • 4.4.1. Using SPARK for design data development
    • 4.4.2. Robustness and SPARK
    • 4.4.3. Contributions to Low-Level Requirement reviews
    • 4.4.4. Contributions to architecture reviews
    • 4.4.5. Contributions to source code reviews
    • 4.4.6. Formal analysis as an alternative to low-level testing
    • 4.4.7. Low-level verification by mixing test and proof ("Hybrid verification")
    • 4.4.8. Alternatives to code coverage when using proofs
    • 4.4.9. Property preservation between source code and object code
    • 4.4.10. SPARK Development Cycle Example
  • 4.5. Parameter Data Items
• 5. Summary of contributions to DO-178C/ED-12C objectives
  • 5.1. Overall summary: which objectives are met
    • 5.1.1. Mapping of AdaCore's Technologies to DO-178C/ED-12C Objectives
  • 5.2. Detailed summary: which activities are supported
    • 5.2.1. Table A-1: Software Planning Process
    • 5.2.2. Table A-2: Software Development Processes
    • 5.2.3. Table A-4: Verification of Outputs of Software Design Process
    • 5.2.4. Table A-5 Verification of Outputs of Software Requirement Process
    • 5.2.5. Table A-6 Testing of Outputs of Integration Process
    • 5.2.6. Table A-7 Verification of Verification Process Results
  • 5.3. AdaCore Tool Qualification and Library Certification
• 6. Bibliography