4. Compliance with ECSS-E-ST-40C

The ECSS‑E‑ST‑40C standard is concerned with software engineering — the principles and techniques underlying the production of code that is reliable, safe, secure, readable, maintainable, portable and efficient. These are the goals that drove the design of the Ada language (and its SPARK subset), whose features assist in designing a modular and robust system architecture and in preventing or detecting errors such as type mismatches or buffer overruns that can arise in other languages.

This chapter explains how Ada and SPARK, together with the relevant AdaCore development and verification tools, can help a space software supplier meet many of the requirements presented in ECSS‑E‑ST‑40C. The section numbers in braces refer to the associated content in 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}

  • "The supplier shall transform the requirements for the software into an architecture that describes the top-level structure; identifies the software components, ensuring that all the requirements for the software item are allocated to the software components and later refined to facilitate detailed design; covers as a minimum hierarchy, dependency, interfaces and operational usage for the software components; documents the process, data and control aspects of the product; describes the architecture static decomposition into software elements such as packages, classes or units; describes the dynamic architecture, which involves the identification of active objects such as threads, tasks and processes; describes the software behavior." {§5.4.3.1a}

    • The Ada and SPARK languages (and thus the GNAT Pro Ada and SPARK Pro toolsuites directly support this requirement. Relevant features include packages, child libraries, subunits, private types, tasking, and object-oriented programming (tagged types). The GNATstub utility (included with GNAT Pro Ada) is useful here; it generates empty package bodies (stubs) from a software design's top-level API (package specs).

4.1.1.2. Software design method {§5.4.3.2}

  • "The supplier shall use a method (e.g., object oriented or functional) to produce the static and dynamic architecture including: software elements, their interfaces and; software elements relationships." {§5.4.3.2a}

    • Ada and SPARK are methodology agnostic and fully support both object-oriented and functional styles.

4.1.1.3. Selection of a computational model for real-time software {§5.4.3.3}

  • "The dynamic architecture design shall be described according to an analytical computational model." {§5.4.3.3a}

    • The Ada and SPARK tasking facility supports a stylistic idiom that is amenable to Rate Monotonic Analysis, allowing static verification that real-time deadlines will be met.

4.1.1.4. Description of software behavior {§5.4.3.4}

  • "The software design shall also describe the behaviour of the software, by means of description techniques using automata and scenarios." {§5.4.3.4a}

    • Ada and SPARK are appropriate target languages for tools that support such techniques.

4.1.1.5. Development and documentation of the software interfaces {§5.4.3.5}

  • "The supplier shall develop and document a software preliminary design for the interfaces external to the software item and between the software components of the software item." {§5.4.3.5a}

    • The supplier can use the Ada / SPARK package facility to specify the interfaces, both external and internal. The contract-based programming features provide additional expressive power, allowing the specification of pre- and postconditions for the subprograms comprising an interface.

4.1.1.6. Definition of methods and tools for software intended for reuse {§5.4.3.6}

  • "The supplier shall define procedures, methods and tools for reuse, and apply these to the software engineering processes to comply with the reusability requirements for the software development." {§5.4.3.6a}

    • Ada and SPARK facilitate reuse via the separate compilation semantics (which allows bottom-up development by reusing existing libraries) and the generic facility (which, for example, allows a module to be defined in a general and type-independent fashion and then instantiated with specific types as needed). The semantics for these features enforces safe reuse:

      • All checks that are performed within a single compilation unit are also enforced across separate compilation boundaries.

      • A post-compilation pre-link check detects and prevents version skew (building an executable where some compilation unit depends on an obsolescent version of another unit).

      • Unlike the situation with C++ templates, a type mismatch in an Ada generic instantiation is detected and prevented at compile time, ensuring consistency between the instantiation and the generic unit.

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}

  • "The supplier shall develop a detailed design for each component of the software and document it." {§5.5.2.1a}

    • Ada / SPARK features, including packages and child units, and thus GNAT Pro for Ada and SPARK Pro, help meet this requirement. The contract-based programming feature (e.g., pre- and postconditions) allows the supplier to express low-level requirements as part of the software architecture, facilitating the low-level design of algorithms.

  • "Each software component shall be refined into lower levels containing software units that can be coded, compiled, and tested." {§5.5.2.1b}

    • Relevant Ada / SPARK features include packages, child units, and subunits.

4.2.1.2. Development and documentation of the software interfaces detailed design {§5.5.2.2}

  • "The supplier shall develop and document a detailed design for the interfaces external to the software items, between the software components, and between the software units, in order to allow coding without requiring further information." {§5.5.2.2a}

    • Ada / SPARK features, including packages and child units, and thus SPARK Pro and GNAT Pro for Ada, help meet this requirement. The contract-based programming feature (e.g., pre- and postconditions) allows the supplier to express low-level requirements as part of the interfaces, facilitating the implementation of algorithms.

4.2.1.3. Production of the detailed design model {§5.5.2.3}

  • "The supplier shall produce the detailed design model of the software components defined during the software architectural design, including their static, dynamic and behavioural aspects." {§5.5.2.3a}

    • Ada / SPARK features such as packages, child units, and contract-based programming, and thus SPARK Pro and GNAT Pro for Ada, help meet this requirement.

4.2.1.4. Software detail design method {§5.5.2.4}

  • "The supplier shall use a design method (e.g. object oriented or functional method) to produce the detailed design including: software units, their interfaces, and; (sic) software units relationships." {§5.5.2.4a}

    • Ada and SPARK are methodology agnostic and fully support both object-oriented and functional styles.

4.2.1.5. Detailed design of real-time software {§5.5.2.5}

  • "The dynamic design model shall be compatible with the computational model selected during the software architectural design model" {§5.5.2.5a}

    • The Ada / SPARK tasking model allows a straightforward mapping from the architectural design (where the system comprises a collection of tasks that interact via protected shared resources) to the detailed design.

  • "The supplier shall document and justify all timing and synchronization mechanisms" {§5.5.2.5b}

    • The Ada / SPARK tasking model supplies the necessary timing and synchronization support.

  • "The supplier shall document and justify all the design mutual exclusion mechanisms to manage access to the shared resources." {§5.5.2.5c}

    • The Ada / SPARK tasking model supplies the necessary mutual exclusion mechanisms (protected types/objects, pragma Atomic). The protected type/object facility prevents certain kinds of race conditions: in state-based mutual exclusion, the state of an object cannot change between the time that a task evaluates the state condition and when it executes the code based on that state. Other race conditions can be detected by the Defects and Vulnerability Analyzer in the GNAT Static Analysis Suite.

  • "The supplier shall document and justify the use of dynamic allocation of resources." {§5.5.2.5d}

    • Ada has a general and flexible mechanism for dynamic memory management, including the ability of the programmer to specify the semantics of allocation and deallocation within a storage pool. This can be used, for example, to define a fragmentation-free strategy for memory management with constant time for allocation and deallocation. The latest version of SPARK includes a facility for safe pointers.

  • "The supplier shall ensure protection against problems that can be induced by the use of dynamic allocation of resources, e.g. memory leaks." {§5.5.2.5e}

    • Ada includes a variety of mechanisms that assist in preventing dynamic memory management issues. The No_Standard_Allocators_After_Elaboration argument to pragma Restrictions produces a run-time check that detects attempts to perform allocations from a standard storage pool after elaboration (initialization). Depending on the program structure, static analysis by the GNAT Static Analysis Suite's Defect and vulnerability Analyzer may be able to determine that this check will never fail.

4.2.1.6. Utilization of description techniques for the software behaviour {§5.5.2.6}

  • "The behavioural design of the software units shall be described by means of techniques using automata and scenarios." {§5.5.2.6a}

    • Ada and SPARK are appropriate target languages for tools that support such techniques.

4.2.2. Coding and testing {§5.5.3}

4.2.2.1. Development and documentation of the software units {§5.5.3.1}

  • "The supplier shall develop and document the following: the coding of each software unit; the build procedures to compile and link software units" {§5.5.3.1a}

    • The GNAT Pro project and gprbuild facility automate the build process and prevent version skew.

4.2.2.2. Software unit testing {§5.5.3.2}

  • "The supplier shall develop and document the test procedures and data for testing each software unit" {§5.5.3.2a}

  • "The supplier shall test each software unit ensuring that it satisfies its requirements and document the test results." {§5.5.3.2b}

  • "The unit test shall exercise: code using boundaries at n-1, n, n+1 including looping instructions while, for and tests that use comparisons; all the messages and error cases defined in the design document; the access of all global variables as specified in the design document; out of range values for input data, including values that can cause erroneous results in mathematical functions; the software at the limits of its requirements (stress testing)." {§5.5.3.2c}

4.2.3. Integration {§5.5.4}

4.2.3.1. Software units and software component integration and testing {§5.5.4.2}

  • "The supplier shall integrate the software units and software components, and test them, as the aggregates are developed, in accordance with the integration plan, ensuring each aggregate satisfies the requirements of the software item and that the software item is integrated at the conclusion of the integration activity." {§5.5.4.2a}

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}

  • "The supplier shall develop and document, for each requirement of the software item in TS [Technical Specification] (including ICD [Interface Control Document]), a set of tests, test cases (inputs, outputs, test criteria) and test procedures ...." {§5.6.3.1a}

  • "Validation shall be performed by test." {§5.6.3.1b}

  • "If it can be justified that validation by test cannot be performed, validation shall be performed by either analysis, inspection or review of design" {§5.6.3.1c}

    • The Defects and Vulnerability Analyzer (see Defects and Vulnerability Analyzer) in the GNAT Static Analysis Suite and/or SPARK Pro may be able to show that a run-time check will always succeed and that no test case will trigger a failure.

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}

  • "The supplier shall develop and document, for each requirement of the software item in RB [Requirements Baseline] (including IRD [Interface Requirements Document]), a set of tests, test cases (inputs, outputs, test criteria) and test procedures ...." {§5.6.4.1a}

  • "Validation shall be performed by test." {§5.6.4.1b}

  • "If it can be justified that validation by test cannot be performed, validation shall be performed by either analysis, inspection or review of design” {§5.6.4.1c}

    • The Defects and Vulnerability Analyzer (see Defects and Vulnerability Analyzer) in the GNAT Static Analysis Suite and/or SPARK Pro may be able to show that a run-time check will always succeed and that no test case will trigger a failure.

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}

  • "The acceptance shall include generation of the executable code from configuration managed source code components and its installation on the target environment." {§5.7.3.3a}

    • The GNAT Pro project and gprbuild facility can assist in the build and installation process.

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}

  • "The supplier shall verify the software detailed design ensuring that: ... 5. testing is feasible, by assessing that: (a) controllability and observability features are identified and included in the detailed design in order to prepare the effective testing of the performance requirements; (b) computationally invariant properties and temporal properties are added within the design; (c) fault injection is possible. ... 7. the design is correct with respect to requirements and interfaces, including safety, security, and other critical requirements; 8. the design implements proper sequence of events, inputs, outputs, interfaces, logic flow, allocation of timing and sizing budgets, and error handling; ..." {§5.8.3.4a}

    • SPARK (and GNATprove) help meet criteria 5, 7, and 8.

4.4.1.2. Verification of code {§5.8.3.5}

  • "The supplier shall verify the software code ensuring at least that: 1. the code is externally consistent with the requirements and design of the software item; 2. there is internal consistency between software units; 3. the code is traceable to design and requirements, testable, correct, and in conformity to software requirements and coding standards; 4. the code that is not traced to the units is justified; 5. the code implements proper events sequences, consistent interfaces, correct data and control flow, completeness, appropriate allocation of timing and sizing budgets; 6. the code implements safety, security, and other critical requirements correctly as shown by appropriate methods; 7. the code is implemented in a way that it cannot result in runtime errors; 8. the effects of any residual runtime errors are controlled through error handling." {§5.8.3.5a}

    • SPARK (and GNATprove) help meet criterion 1.

    • Ada's strong typing and interface checks (and thus GNAT Pro for Ada) help meet criterion 2.

    • For criterion 3, the Defects and Vulnerability Analyzer (see Defects and Vulnerability Analyzer) in the GNAT Static Analysis Suite and/or SPARK Pro can help verify correctness, and the GNATcheck utility included in the GNAT Static Analysis Suite (see GNATcheck) can enforce conformance with a coding standard.

    • For criterion 5, Ada's strong typing and interface checks, as well as SPARK and GNATprove, can help show consistent interfaces and correct data flow.

    • The Defects and Vulnerability Analyzer (see Defects and Vulnerability Analyzer) in the GNAT Static Analysis Suite, SPARK Pro, and the standard semantic checks performed by the GNAT Pro compiler can help meet criterion 6.

    • The GNAT Static Analysis Suite and SPARK / GNATprove can statically detect potential run-time errors and thereby help meet criterion 7.

    • Ada's exception handling facility can help meet criterion 8.

  • "The supplier shall verify that the following code coverage is achieved:

    Code coverage versus criticality category

    A

    B

    C

    D

    Source code statement coverage

    100.00%

    100.00%

    TBA

    TBA

    Source code decision coverage

    100.00%

    100.00%

    TBA

    TBA

    Source code modified condition and decision coverage

    100.00%

    TBA

    TBA

    TBA

    Note: 'TBA' means that the value is to be agreed with the customer and measured as per ECSS‑Q‑ST‑80C clause 6.3.5.2." {§5.8.3.5b}

    • The GNATcoverage tool (see GNATcoverage) in the GNAT Dynamic Analysis Suite can help meet this requirement.

  • "The supplier shall measure code coverage by analysis of the results of the execution of tests." {§5.8.3.5c}

    • The GNATcoverage tool (see GNATcoverage) in the GNAT Dynamic Analysis Suite can help meet this requirement.

  • "If it can be justified that the required percentage cannot be achieved by test execution, then analysis, inspection or review of design shall be applied to the non-covered code." {§5.8.3.5d}

    • The GNATcoverage tool (see GNATcoverage) in the GNAT Dynamic Analysis Suite can help meet this requirement.

  • "In case the traceability between source code and object code cannot be verified, the supplier shall perform additional code coverage analysis on object code level as follows:

    Code coverage versus criticality category

    A

    B

    C

    D

    Object code coverage

    100.00%

    N/A

    N/A

    N/A

    Note: 'N/A' means not applicable.

    Note: The use of some compiler optimization options can make the traceability between source code and object code not possible." {§5.8.3.5e}

    • The GNATcoverage tool (see GNATcoverage) in the GNAT Dynamic Analysis Suite can help meet this requirement.

    • AdaCore can prepare an analysis of traceability between source and object code; the company has provided this to customers in connection with certification under the DO-178C/ED-12C standard for airborne software for the commercial aviation industry.

  • "The supplier shall verify source code robustness. AIM: use static analysis for the errors that are difficult to detect at run-time." {§5.8.3.5f}

    • Errors such as division by zero, null pointer dereferencing, array indices out of bounds, and many others are flagged at run-time by raising an exception. Effective practice is to keep these checks enabled during development and then, after verifying either statically or through sufficient testing that the run-time checks are not needed, disable the checks in the final code for maximal efficiency.

    • The Defects and Vulnerability Analyzer (see Defects and Vulnerability Analyzer) in the GNAT Static Analysis Suite will detect such errors as well as many others, including suspicious constructs that, although legitimate Ada, are likely logic errors.

    • SPARK Pro will enforce the SPARK subset and can be used to demonstrate absence of run-time errors.

    • The GNATstack tool in GNAT Pro computes the potential maximum stack usage for each task in a program. Combining the result with a separate analysis showing the maximal depth of recursion, the developer can allocate sufficient stack space for program execution and prevent stack overflow.

4.4.1.3. Schedulability analysis for real-time software {§5.8.3.11}

  • "As part of the verification of the software requirements and architectural design, the supplier shall use an analytical model to perform a schedulability analysis and prove that the design is feasible." {§5.8.3.11a}

    • The Ada Ravenscar profile restricts the tasking model to enable precise schedulability analysis, including Rate-Monotonic Analysis (RMA).

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}

  • "The SOS [Software Operation Support] entity shall establish procedures for receiving, recording, resolving, tracking problems, and providing feedback." {§5.9.2.3a}

    • In the event that a product problem is due to a defect in an AdaCore tool (e.g., a code generation bug), AdaCore has a rigorous QA process for responding to and resolving such issues. The sustained branch service, which is included with a GNAT Pro Assurance subscription, helps by ensuring that a specific version of the toolchain is maintained over the lifetime of the supplier's project.

  • "The SOS entity shall ensure that information regarding problems that can have an impact on security is protected." {§5.9.2.3b}

    • AdaCore's internal processes for maintaining sensitive data help to meet this criterion.

4.5.2. Software operation support {§5.9.4}

4.5.2.1. Problem handling {§5.9.4.2}

  • "Encountered problems shall be recorded and handled in accordance with the applicable procedures." {§5.9.4.2a}

    • As described above in connection with clause 5.9.2.3, AdaCore's QA process, and more specifically the GNAT Pro Assurance sustained branch service with its management of Known Problems, can help meet this requirement when an issue arises that is due to an AdaCore tool.

4.5.2.2. Vulnerabilities in operations {§5.9.4.3}

  • "During operations, security vulnerabilities, threats and exploits shall be: 1. continuously monitored; 2. subject to further security analysis when evaluated relevant to the security of the system; 3. maintained for auditing purposes even when evaluated not relevant to the security of the system." {§5.9.4.3a}

    • The ability to express security-related requirements as contracts in the Ada source code, with run-time checks when needed, helps to meet criterion 1.

4.5.3. User support §5.9.5

4.5.3.1. Provisions of work-around solutions {§5.9.5.3}

  • "If a reported problem has a temporary work-around solution before a permanent solution can be released, the SOS entity shall give to the originator of the problem report the option to use it." {§5.9.5.3a}

    • As part of the GNAT Pro Assurance sustained branch service, AdaCore can supply work-arounds to critical problems prior to releasing a permanent solution.

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}

  • "The maintainer shall propose solutions to be able to implement and upload modifications to the spacecraft up to its end of life." {§5.10.2.2a}

    • AdaCore's sustained branch service, which is included with a GNAT Pro Assurance subscription, in effect means that the compilation environment will receive support and not become obsolescent.

4.6.2. Modification implementation {§5.10.4}

4.6.2.1. Invoking of software engineering processes for modification implementation {§5.10.4.3}

  • "The maintainer shall apply the software engineering processes specified in clauses 5.3 to 5.8 and 5.11 that are relevant to the scope of the modifications, using the tailoring applied during the development of the software." {§5.10.4.3a}

    • The Ada and SPARK languages have specific features that support the design of modular, maintainable software with high cohesion and low coupling. These include encapsulation (private types, separation of specification from implementation), hierarchical child libraries, and object-oriented programming (tagged types). By exploiting these features and utilizing GNAT Pro for Ada and SPARK Pro, the developer can localize the impact of maintenance changes.

    • The GNAT Static and Dynamic Analysis Suites can ensure that any modifications meet the verification criteria applicable to the original software.

4.7. Software security process {§ 5.11}

4.7.1. Process implementation {§ 5.11.2}

  • "A software security management plan shall be produced documenting: ... 7. the tools, methods and procedures to be used...." {§ 5.11.2a}

    • The Ada and SPARK languages, GNAT Pro for Ada, the GNAT Static and Dynamic Analysis Suites, and the SPARK Pro toolset support the software security management plan.

4.7.2. Software security analysis {§ 5.11.3}

  • "The methods to be used for the security analysis shall be identified as part of the planning of the project." {§ 5.11.3b}

    • The Ada and SPARK languages, GNAT Pro for Ada, the GNAT Static and Dynamic Analysis Suites, and the SPARK Pro toolset help meet this requirement. For example:

      • Ada's compile-time checks prevent unsafe practices such as treating an integer value as a pointer.

      • The Defects and Vulnerability Analyzer in the GNAT Static Analysis Suite can detect a number of dangerous software errors in the MITRE Corporation's Common Weakness Enumeration.

      • The SPARK language and SPARK Pro can enforce security-related properties such as correct information flows and absence of run-time errors.

      • GNATfuzz can be used to stress test the software with malformed input values.

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}

  • "The security assurance requirements shall determine the type and extent of security verification and validation activities, including testing, to be conducted.... Security verification and validation activities can include, for example, fuzzing tests...." {§ 5.11.5.1c}

    • The Ada and SPARK languages, GNAT Pro for Ada, the GNAT Static and Dynamic Analysis Suites, and the SPARK Pro toolset help meet this requirement.

4.7.3.2. Security in the detailed design and implementation engineering {§ 5.11.5.3}

  • "The software security analysis shall be used during verification and validation activities to evaluate iteratively residual vulnerabilities and to reassess security risks." {§ 5.11.5.3b}

4.8. Software code verification {Annex U (informative)}

  • "The following checks are expected to be performed on the software code:

    1. the code implements numerical protection mechanisms (e.g. against overflow and underflow, division by zero);

    2. the code does not perform out of bounds accesses - e.g. underrun or overrun of buffers, arrays or strings;

    3. the code does not include any infinite loop other than the main loop of the software and the main loops of cyclic tasks;

    4. the code appropriately uses arithmetical and logical operators (e.g. arithmetical OR vs. logical OR);

    5. implicit type conversions do not lead to arithmetical errors;

    6. the lifetime of variables is consistent with their use;

    7. the code makes proper use of static/global functions/variables to enforce the correct level of visibility;

    8. the code makes proper use of volatile variables for all variables that can be modified asynchronously (e.g. hardware access, memory-mapped I/O);

    9. the code does not perform invalid memory accesses (e.g. NULL dereferences);

    10. the code does not access uninitialized variables;

    11. the code does not perform unused assignments, unless this is done to trigger HW side-effects;

    12. there are no memory leaks;

    13. pointer arithmetic is justified and types of operands are consistent;

    14. the code does not lead to race conditions." {§ U.2}

Table 14 shows how AdaCore's technologies help meet these requirements:

Table 14 Verification Support

Verification check #

Technology

Explanation

1

Ada language, GNAT Pro for Ada, GNAT Pro Assurance

Run-time check [1]

SPARK language, SPARK Pro

Static check

Defects and Vulnerability Analyzer (in GNAT Static Analysis Suite)

Static check [2]

2

Ada language, GNAT Pro for Ada, GNAT Pro Assurance

Run-time check [1]

SPARK language, SPARK Pro

Static check

Defects and Vulnerability Analyzer (in GNAT Static Analysis Suite)

Static check [2]

3

Defects and Vulnerability Analyzer (in GNAT Static Analysis Suite)

Static check [2]

GNATcheck (in GNAT Static Analysis Suite)

User-defined rule

SPARK language, SPARK Pro

Static check

4

Ada language, GNAT Pro for Ada, GNAT Pro Assurance SPARK language, SPARK Pro

Static check

GNATcheck (in GNAT Static Analysis Suite)

User-defined rule

5

Ada language, GNAT Pro for Ada, GNAT Pro Assurance SPARK language, SPARK Pro

Static check

Defects and Vulnerability Analyzer (in GNAT Static Analysis Suite)

Static check [2]

6

Ada language, GNAT Pro for Ada, GNAT Pro Assurance SPARK language, SPARK Pro

Static check

7

Ada language, GNAT Pro for Ada, GNAT Pro Assurance SPARK language, SPARK Pro

Static check

8

Defects and Vulnerability Analyzer (in GNAT Static Analysis Suite)

Static check [2]

9

Ada language, GNAT Pro for Ada, GNAT Pro Assurance

Run-time check [1]

SPARK language, SPARK Pro

Static check

Defects and Vulnerability Analyzer (in GNAT Static Analysis Suite)

Static check [2]

10

SPARK language, SPARK Pro

Static check

Defects and Vulnerability Analyzer (in GNAT Static Analysis Suite)

Static check [2]

11

Defects and Vulnerability Analyzer (in GNAT Static Analysis Suite)

Static check [2]

12

Defects and Vulnerability Analyzer (in GNAT Static Analysis Suite)

Static check [2]

Ada Language, GNAT Pro for Ada, GNAT Pro Assurance

Run-time check [3]

GNATstack (for preventing stack overflow)

Static check

13

Ada language, GNAT Pro for Ada, GNAT Pro Assurance SPARK language, SPARK Pro

Static check

14

Defects and Vulnerability Analyzer (in GNAT Static Analysis Suite)

Static check [2]

4.9. Compliance Summary

Table 15 shows how AdaCore's technologies support the requirements in ECSS-E-ST-40C:

Table 15 Technology Support for ECSS-E-ST-40C Compliance

Technology

§5.4

§5.5

§5.6

§5.7

§5.8

§5.9

§5.10

§5.11

Annex U

Ada language

✓

✓

✓

✓

✓

✓

✓

SPARK language

✓

✓

✓

✓

✓

✓

GNAT Pro for Ada

✓

✓

✓

✓

✓

✓

✓

✓

SPARK Pro

✓

✓

✓

✓

✓

✓

✓

GNAT Static Analysis Suite

✓

✓

✓

✓

✓

✓

GNAT Dynamic Analysis Suite

✓

✓

✓

✓

✓

GNAT Pro Assurance

✓

✓

✓

✓

✓

✓

✓

✓

✓