AdaCore Technologies for Space Systems Software

Supporting Qualification for ECSS-E-ST-40C and ECSS-Q-ST-80C

Download PDF Download EPUB

About the Authors

Benjamin M. Brosgol

Dr. Brosgol is a senior member of the technical staff at AdaCore. He has been involved with programming language design and implementation throughout his career, concentrating on languages and technologies for high-assurance systems. He was a Distinguished Reviewer during the original Ada development, a member of the language design team in the Ada 95 revision, and a member of the Expert Group for the Real-Time Specification for Java under the Java Community Process. He has published dozens of journal articles and delivered conference presentations on topics including the avionics software standard DO ‑ 178C/ED ‑ 12C, the Ada and SPARK languages, real-time software technologies, object-oriented methodologies, and the FACE® (Future Airborne Capabilities Environment) approach to software portability.

Jean-Paul Blanquart

Dr. Blanquart is a recognized authority on computer-based systems safety and dependability, with a decades-long career that spans academic research (LAAS-CNRS, Toulouse, France) and the space industry (Airbus Defence and Space). He was a member of the ECSS Working Groups in charge of revision 1 of ECSS-Q-ST-80C and ECSS-Q-HB-80-03A (and also the dependability and safety standards ECSS-Q-ST-30C and ECSS-Q-ST-40C). He has been an active member of a French cross-domain Working Group on safety and safety standards since its creation in 2010. This Working Group gathers industrial safety experts and related tool providers from domains that include automotive, aviation, defense, nuclear, industrial processes, railway and space.

Foreword

"Failure is not an option"

Gene Kranz (NASA) in the film Apollo 13

Software development presents daunting challenges when the resulting system needs to operate reliably, safely, and securely while meeting hard real-time deadlines on a memory-limited target platform. Correct program execution can literally be a matter of life and death, but such is the reality facing developers of space software systems. A project's ability to produce high-assurance software in a cost-effective manner depends on two factors:

• Effective processes for managing the software and system life cycles, with well-defined activities for planning, controlling, and monitoring the work; and

• Effective technologies (programming languages, development and verification tools, version control systems, etc.) to support the software life-cycle processes.

For safety-critical application domains, the first factor is typically anticipated by a regulatory authority in the form of certification / qualification standards such as are found in the civil aviation and nuclear industries. In the space domain the ECSS software-related standards play a similar role, with the current set of documents based on decades of experience with space system development. In particular, the software engineering standard ECSS‑E‑ST‑40C and the software product assurance standard ECSS‑Q‑ST‑80C provide a framework in which software suppliers and customers can interact, with a clear statement and understanding of processes and responsibilities.

Technologies, and more specifically the choice of programming language(s) and supporting toolsuites, directly affect the ease or difficulty of developing, verifying, and maintaining quality software. The state of the art in software engineering has made large strides over the years, with programming language / methodology advances in areas such as modularization and encapsulation. Nevertheless, the key messages have stayed constant:

• The programming language should help prevent errors from being introduced in the first place; and

• If errors are present, the language rules should detect them early in the software life cycle, when defects are easiest and least expensive to correct.

These messages come through clearly in the Ada programming language, which was designed from the start to enforce sound software engineering principles, catching errors early and avoiding pitfalls such as buffer overrun that arise in other languages. Ada has evolved considerably since it first emerged in the mid-1980s, for example adding Object-Oriented Programming support in Ada 95, but each new version has kept true to the original design philosophy.

AdaCore's Ada-based tools have been helping developers design, develop and maintain high-assurance software since the mid 1990s, in domains that include space systems, commercial and military avionics, air traffic control, train systems, automotive, and medical devices. This document summarizes AdaCore's language and tool technologies and shows how they can help space software suppliers meet the requirements in ECSS‑E‑ST‑40C and ECSS‑Q‑ST‑80C. With effective processes as established by these standards, and effective technologies as supplied by AdaCore, software suppliers will be well equipped to meet the challenges of space software development.

Benjamin M. Brosgol

AdaCore

Bedford, Massachusetts USA

November 2021

Jean-Paul Blanquart

Airbus Defence and Space

Toulouse, France

November 2021

Foreword to V2.1

In the years since the initial version of this document was published, both ECSS‑E‑ST‑40C and ECSS‑Q‑ST‑80C have been revised, and AdaCore's products have evolved to meet the growing demands for, and challenges to, high assurance in mission-critical real-time software. This new edition reflects the current (2025) versions of ECSS‑E‑ST‑40C, ECSS‑Q‑ST‑80C, and AdaCore's offerings. Among other updates and enhancements to the company's products, 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.

As editor of this revised edition, I would like to thank my AdaCore colleagues Olivier Appéré and Vasiliy Fofanov, as well as co-author Jean-Paul Blanquart, for their detailed and helpful reviews and suggestions.

For up-to-date information on AdaCore support for developing space software, please visit [1].

Benjamin M. Brosgol, AdaCore

Bedford, Massachusetts USA

December 2025

• 1. Introduction
  • 1.1. ECSS-E-ST-40C: Space engineering / Software
  • 1.2. ECSS-Q-ST-80C: Space product assurance / Software product assurance
  • 1.3. ECSS Handbooks
• 2. Programming Languages for Space Software
  • 2.1. Ada
    • 2.1.1. Ada language overview
    • 2.1.2. Ada language background
    • 2.1.3. Scalar ranges
    • 2.1.4. Contract-based programming
    • 2.1.5. Programming in the large
    • 2.1.6. Generic templates
    • 2.1.7. Object-Oriented Programming (OOP)
    • 2.1.8. Concurrent programming
    • 2.1.9. Systems programming
    • 2.1.10. Real-time programming
    • 2.1.11. Time and Space Analysis
    • 2.1.12. High-integrity systems
    • 2.1.13. Enforcing a coding standard
    • 2.1.14. Ada and the ECSS Standards
  • 2.2. SPARK
    • 2.2.1. SPARK Basics
    • 2.2.2. Ease of Adoption
    • 2.2.3. Levels of Adoption of Formal Methods
      • 2.2.3.1. Stone level: Valid SPARK
      • 2.2.3.2. Bronze level: Initialization and correct data flow
      • 2.2.3.3. Silver level: Absence of run-time errors (AORTE)
      • 2.2.3.4. Gold level: Proof of key integrity properties
      • 2.2.3.5. Platinum level: Full functional correctness
    • 2.2.4. Hybrid Verification
    • 2.2.5. SPARK and the ECSS Standards
• 3. Tools for Space Software Development
  • 3.1. AdaCore Tools and the Software Life Cycle
  • 3.2. Static Verification: SPARK Pro
    • 3.2.1. Powerful Static Verification
    • 3.2.2. Minimal Run-Time Footprint
    • 3.2.3. CWE Compatibility
    • 3.2.4. SPARK Pro and the ECSS Standards
  • 3.3. GNAT Pro Development Environment
    • 3.3.1. GNAT Pro Enterprise
    • 3.3.2. GNAT Pro Assurance
      • 3.3.2.1. Sustained Branches
      • 3.3.2.2. Source to Object Traceability
      • 3.3.2.3. Compliance with the ECSS Standards
    • 3.3.3. Libadalang
    • 3.3.4. GNATstack
      • 3.3.4.1. Compliance with the ECSS Standards
    • 3.3.5. GNAT Pro for Rust
    • 3.3.6. Integrated Development Environments (IDEs)
      • 3.3.6.1. GNAT Studio
      • 3.3.6.2. VS Code Extensions for Ada and SPARK
      • 3.3.6.3. Eclipse Support – GNATbench
      • 3.3.6.4. GNATdashboard
    • 3.3.7. GNAT Pro and the ECSS Standards
  • 3.4. Static Verification: GNAT Static Analysis Suite (GNAT SAS)
    • 3.4.1. Defects and Vulnerability Analyzer
      • 3.4.1.1. CWE Compatibility
      • 3.4.1.2. Compliance with the ECSS Standards
    • 3.4.2. GNATmetric
      • 3.4.2.1. Compliance with the ECSS Standards
    • 3.4.3. GNATcheck
      • 3.4.3.1. Compliance with the ECSS Standards
  • 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.5.6. GNAT Dynamic Analysis Suite and the ECSS Standards
  • 3.6. Support and Expertise
• 4. Compliance with ECSS-E-ST-40C
  • 4.1. Software requirements and architecture engineering process {§5.4}
    • 4.1.1. Software architecture design {§5.4.3}
      • 4.1.1.1. Transformation of software requirements into a software architecture {§5.4.3.1}
      • 4.1.1.2. Software design method {§5.4.3.2}
      • 4.1.1.3. Selection of a computational model for real-time software {§5.4.3.3}
      • 4.1.1.4. Description of software behavior {§5.4.3.4}
      • 4.1.1.5. Development and documentation of the software interfaces {§5.4.3.5}
      • 4.1.1.6. Definition of methods and tools for software intended for reuse {§5.4.3.6}
  • 4.2. Software design and implementation engineering process {§5.5}
    • 4.2.1. Design of software items {§5.5.2}
      • 4.2.1.1. Detailed design of each software component {§5.5.2.1}
      • 4.2.1.2. Development and documentation of the software interfaces detailed design {§5.5.2.2}
      • 4.2.1.3. Production of the detailed design model {§5.5.2.3}
      • 4.2.1.4. Software detail design method {§5.5.2.4}
      • 4.2.1.5. Detailed design of real-time software {§5.5.2.5}
      • 4.2.1.6. Utilization of description techniques for the software behaviour {§5.5.2.6}
    • 4.2.2. Coding and testing {§5.5.3}
      • 4.2.2.1. Development and documentation of the software units {§5.5.3.1}
      • 4.2.2.2. Software unit testing {§5.5.3.2}
    • 4.2.3. Integration {§5.5.4}
      • 4.2.3.1. Software units and software component integration and testing {§5.5.4.2}
    • 4.2.4. Validation activities with respect to the technical specification {§5.6.3}
      • 4.2.4.1. Development and documentation of a software validation specification with respect to the technical specification {§5.6.3.1}
    • 4.2.5. Validation activities with respect to the requirements baseline {§5.6.4}
      • 4.2.5.1. Development and documentation of a software validation specification with respect to the requirements baseline {§5.6.4.1}
  • 4.3. Software delivery and acceptance process {§5.7}
    • 4.3.1. Software acceptance {§5.7.3}
      • 4.3.1.1. Executable code generation and installation {§5.7.3.3}
  • 4.4. Software verification process {§5.8}
    • 4.4.1. Verification activities {§5.8.3}
      • 4.4.1.1. Verification of the software detailed design {§5.8.3.4}
      • 4.4.1.2. Verification of code {§5.8.3.5}
      • 4.4.1.3. Schedulability analysis for real-time software {§5.8.3.11}
  • 4.5. Software operation process {§5.9}
    • 4.5.1. Process implementation {§5.9.2}
      • 4.5.1.1. Problem handling procedures definition {§5.9.2.3}
    • 4.5.2. Software operation support {§5.9.4}
      • 4.5.2.1. Problem handling {§5.9.4.2}
      • 4.5.2.2. Vulnerabilities in operations {§5.9.4.3}
    • 4.5.3. User support §5.9.5
      • 4.5.3.1. Provisions of work-around solutions {§5.9.5.3}
  • 4.6. Software maintenance process {§5.10}
    • 4.6.1. Process implementation {§5.10.2}
      • 4.6.1.1. Long term maintenance for flight software {§5.10.2.2}
    • 4.6.2. Modification implementation {§5.10.4}
      • 4.6.2.1. Invoking of software engineering processes for modification implementation {§5.10.4.3}
  • 4.7. Software security process {§ 5.11}
    • 4.7.1. Process implementation {§ 5.11.2}
    • 4.7.2. Software security analysis {§ 5.11.3}
    • 4.7.3. Security activities in the software life cycle {§ 5.11.5}
      • 4.7.3.1. Security in the requirements baseline {§ 5.11.5.1}
      • 4.7.3.2. Security in the detailed design and implementation engineering {§ 5.11.5.3}
  • 4.8. Software code verification {Annex U (informative)}
  • 4.9. Compliance Summary
• 5. Compliance with ECSS-Q-ST-80C
  • 5.1. Software product assurance programme implementation {§5}
    • 5.1.1. Software product assurance programme management {§5.2}
      • 5.1.1.1. Quality requirements and quality models {§5.2.7}
    • 5.1.2. Tools and supporting environment {§5.6}
      • 5.1.2.1. Methods and tools {§5.6.1}
      • 5.1.2.2. Development environment selection {§5.6.2}
  • 5.2. Software process assurance {§6}
    • 5.2.1. Requirements applicable to all software engineering processes {§6.2}
      • 5.2.1.1. Handling of critical software {§6.2.3}
      • 5.2.1.2. Verification {§6.2.6}
      • 5.2.1.3. Software security {§6.2.9}
      • 5.2.1.4. Handling of security sensitive software {§ 6.2.10}
    • 5.2.2. Requirements applicable to individual software engineering processes or activities {§6.3}
      • 5.2.2.1. Coding {§6.3.4}
      • 5.2.2.2. Testing and validation {§6.3.5}
      • 5.2.2.3. Maintenance {§6.3.9}
  • 5.3. Software product quality assurance {§7}
    • 5.3.1. Product quality objectives and metrication {§7.1}
      • 5.3.1.1. Assurance activities for product quality requirements {§7.1.3}
      • 5.3.1.2. Basic metrics {§7.1.5}
    • 5.3.2. Product quality requirements {§7.2}
      • 5.3.2.1. Design and related documentation {§7.2.2}
      • 5.3.2.2. Test and validation documentation {§7.2.3}
  • 5.4. Compliance Summary
• 6. Abbreviations

Bibliography

[1]

AdaCore. AdaCore + Space. URL: https://www.adacore.com/industries/space.