6. Technology Annex¶
This annex summarizes how AdaCore's tools and technologies support the various techniques and measures defined in Annex D of EN 50128. The qualification status for tools, and certifiability for run-time libraries, are also noted.
6.1. Ada Programming Language¶
See Ada.
6.1.1. Qualification¶
Although there is no qualification of a language per se, the Ada language is standardized through an official process managed by an ISO committee, IEC/ISO 8652. AdaCore's Ada compilers and tools have reference and user documentation that precisely describes the expected behavior, including the effects of implementation-defined features.
6.1.2. Annex D References¶
D.2 Analyzable Programs
D.4 Boundary Value Analysis
D.14 Defensive Programming
D.18 Equivalence Classes and Input Partition Testing
D.24 Failure Assertion Programming
D.33 Information Hiding / Encapsulation
D.34 Interface Testing
D.35 Language Subset
D.38 Modular Approach
D.49 Strongly Typed Programming Languages
D.53 Structured Programming
D.54 Suitable Programming Languages
D.57 Object Oriented Programming
D.60 Procedural Programming
6.2. GNAT Pro Assurance Toolsuite¶
6.2.1. Qualification¶
GNAT Pro compiler family
The GNAT Pro compilers for Ada and for C are qualified at class T3. AdaCore can provide documentation attesting to various aspects such as service history, development standard, and testing results. This documentation has been submitted and accepted in past certification activities. T3 qualification material can also be developed for the GNAT Pro for C++ and GNAT Pro for Rust compilers.
Since compilers are large and complex pieces of software, bugs can be detected (and subsequently corrected) after a particular version has been chosen. Following the requirements stated in 6.7.4.11, however, a corrected version of the compiler cannot be deployed without specific justification. AdaCore offers a dedicated service – GNAT Pro Assurance – on a specified version of the technology, which provides critical problem fixes (or workaround suggestions) as well as detailed descriptions of the changes. Using GNAT Pro Assurance, a customer can integrate a corrected version of a specific compiler release into their development infrastructure without the risk of regressions from unwanted updates.
See GNAT Pro Assurance.
GNATstack
GNATstack can be qualified as a class T2 tool.
6.2.2. Run-Time Certification¶
Certification material up to SIL 4 can be developed for the Light and Light-Tasking run-time libraries.
6.2.3. Annex D References¶
D.10 Data Flow Analysis
D.15 Coding Standards and Style Guide
D.18 Equivalence Classes and Input Partition Testing
D.35 Language Subset
6.3. SPARK Language and Toolsuite¶
See SPARK.
6.3.1. Qualification¶
The SPARK Pro toolsuite can be qualified at class T2.
6.3.2. Annex D References¶
The SPARK language and toolset can contribute to the deployment or implementation of the following techniques:
D.2 Analyzable Programs
D.4 Boundary Value Analysis
D.10 Data Flow Analysis
D.14 Defensive Programming
D.18 Equivalence Classes and Input Partition Testing
D.24 Failure Assertion Programming
D.28 Formal Methods
D.29 Formal Proof
D.34 Interface Testing
D.35 Language Subset
D.38 Modular Approach
D.57 Object Oriented Programming
6.4. GNAT Static Analysis Suite¶
See GNAT Static Analysis Suite (GNAT SAS).
6.4.1. Defects and Vulnerability Analysis¶
6.4.1.1. Qualification¶
GNAT SAS's defects and vulnerability analysis tool can be qualified at class T2. It has a long cross-industry track record and has been qualified under other standards in the past, such as DO-178B/C as a verification tool/TQL5.
6.4.1.2. Annex D References¶
GNAT SAS's defects and vulnerability analysis tool can contribute to the deployment or implementation of the following techniques:
D.2 Analyzable Programs
D.4 Boundary Value Analysis
D.8 Control Flow Analysis
D.10 Data Flow Analysis
D.14 Defensive Programming
D.18 Equivalence Classes and Input Partition Testing
D.24 Failure Assertion Programming
D.32 Impact Analysis
6.4.2. Basic Static Analysis tools¶
The basic tools are GNATcheck and GNATmetric.
6.4.2.1. Qualification¶
These tools can be qualified at class T2. GNATcheck has been qualified under other standards as well, such as DO-178B/C as a verification tool/TQL5.
6.4.2.2. Annex D References¶
D.2 Analyzable Programs
D.14 Defensive Programming
D.15 Coding Standard and Style Guide
D.35 Language Subset
D.37 Metrics
6.5. GNAT Dynamic Analysis Suite¶
This suite comprises GNATtest, GNATemulator, GNATcoverage, GNATfuzz, and TGEN.
See GNAT Dynamic Analysis Suite (GNAT DAS).
6.5.1. Qualification¶
GNATtest, GNATemulator and GNATcoverage can be qualified at class T2. GNATcoverage has been qualified under other standards as well, such as DO-178B/C as a verification tool/TQL5.
6.5.2. Annex D References¶
D.50 Structure Based Testing
Bibliography