Index

A

Absence of Run-Time Errors (AORTE) Ada language 'Valid attribute Arrays Benefits Concurrent programming, [1], [2] Contract-based programming, [1], [2], [3] Coupling between modules Dimensionality checking Dynamic dispatching (primitive Endianness Generic templates, [1] High-integrity systems, [1] History, [1] Information hiding Interface / implementation separation, [1] Interfacing with C Memory safety, [1] Modulatization Numeric types Object-Oriented Programming (OOP), [1], [2], [3] Package feature package Interfaces Packages Parameter checking Pointers Post'Class aspect Postconditions, [1] pragma Restrictions, [1] Pre'Class aspect Preconditions, [1] Prevention of buffer overflow, [1] Prevention of dangling references, [1] Prevention of null pointer Prevention of null pointer dereferencing Prevention of vulnerabilities, [1] Programming in the large, [1], [2] Protected object / Protected type Real-time programming, [1] Representation clause Scalar ranges, [1] Specifying data representation Strong typing, [1], [2] Support for Analyzable Programs (D.2) Support for Annex D techniques (summary) Support for Boundary Value Analysis (D.4) Support for Defensive Programming (D.14), [1] Support for Information Encapsulation (D.33) Support for Interface Testing (D.34) Support for Modular Approach (D.38), [1] Support for Object Oriented Programming Languages (D.57) Support for Procedural Programming (D.60) Support for Strongly Typed Programming Languages (D.49) Support for Structured Programming (D.53) Support for Suitable Programming Languages (D.54) Systems programming, [1] Task object / task type

AdaCore Support services Training and consulting services and DO-278A/ED-109A Annex D Analyzable Programs (D.2) Boundary Value Analysis (D.4) Coding Standards and Style Guide (D.15) Control Flow Analysis (D.8) Data Flow Analysis (D.10) Defensive Programming (D.14) Error Guessing (D.20) Failure Assertion Programming (D.24) Formal Methods (D.28) Impact Analysis (D.32) Information Encapsulation (D.33) Interface Testing (D.34) Language Subset (D.35) Metrics (D.37) Modular Approach (D.38) Object Oriented Programming (D.57) Procedural Programming (D.60) Structure Based Testing (D.50) Structured Programming (D.53) Suitable Programming Languages (D.54) ARM processor support (by GNAT Pro)

B

Babbage (Charles) Bare metal support (by GNAT Pro)

Buffer overflow, [1] Byron (Lord George)

C

C language support, [1] C++ language support CENELEC CENELEC EN 50716:2023 standard Certifiable profile, [1] Support for Language Subset (D.35) Child package Support for Modular Approach (D.38) code reviews Code Standard enforcement GNATcheck Common Criteria security standard, [1] Common Weakness Enumeration CWE 1061 CWE 1074 CWE 1086 CWE 1106 CWE 1127 CWE 1325, [1], [2] CWE 248, [1], [2] CWE 252 CWE 362, [1] CWE 366, [1] CWE 367, [1] CWE 396 CWE 397 CWE 401, [1], [2], [3], [4], [5] CWE 415, [1], [2], [3], [4] CWE 416, [1], [2], [3], [4] CWE 457 CWE 459, [1] CWE 478, [1] CWE 496 CWE 547 CWE 563 CWE 567 CWE 590 CWE 667 CWE 670 CWE 674 CWE 685 CWE 754, [1] CWE 758 CWE 770 CWE 771, [1], [2] CWE 789 CWE 843

Considerations Considerations for CNS/ATM Systems consistency with GNAT SAS Contract-based programming Support for Failure Assertion Programming (D.24) Contract_Cases aspect

D

Data and control coupling coverage GNATcoverage Decision Coverage (MC/DC) Defects and Vulnerability Analysis Qualification Support for Annex D techniques (summary) Defects and vulnerability analysis (in GNAT SAS), [1] dereferencing Design Assurance Level (DAL) Dimension consistency analysis DO-178C/ED-12C Compliance Executable Object Code (EOC) High-Level Requirement (HLR) Low-Level Requirement (LLR) DO-178C/ED-12C and AdaCore technologies Summary Table A-1: Table A-2: Software Development Processes Table A-4: Table A-5: Verification of Outputs of Software Requirement Process Table A-6: Table A-7:

DO-248C/ED-94C: Supporting Information for DO-178C/ED-12C DO-278A/ED-109A: Software Integrity Assurance DO-326A/ED-202A: Airworthiness Security Process DO-330/ED-215: Software Tool Qualification Considerations, [1], [2] DO-331/ED-218: Model-Based Development and Verification, [1], [2] DO-332/ED-217: Object-Oriented Technology and, [1], [2], [3], [4], [5], [6], [7], [8], [9], [10], [11], [12], [13], [14], [15], [16], [17], [18], [19] DO-332/ED-217: Object-Oriented Technology and Related, [1] DO-332/ED-217: Object-Oriented Technology and Related Techniques Traceability DO-333/ED-216: Formal Methods, [1], [2], [3], [4] DO-356A/ED-203A: Airworthiness Security Methods and

E

Eclipse IDE, [1], [2] Embedded system support (by GNAT Pro) EN 50126 EN 50128 Annex A (Criteria for the Selection of Techniques and Measures) Annex B (Key software roles and responsibilities) Annex C (Documents Control Summary) Annex D (Bibliography of techniques) Annex ZZ Clause 4 (Objectives, conformance and software safety integrity levels) Clause 5 (Software management and organization) Clause 6 (Software assurance) Clause 7 (Generic software development) Clause 8 (Development of application data or algorithms) Clause 9 (Software deployment and maintenance) Structure of the standard

EN 50129 EN 50657 EN 50716 excluding OOT Checking source code accuracy and Checking worst-case stack consumption with Coding with Ada 2012 Compiling with the GNAT Pro compiler Contract-based programming Implementation of hardware / software Integration of C components with Ada Low-level requirements Structural code coverage with GNATcoverage Using Ada during the design process Using GNATemulator for low-level and Executable Object Code (EOC)

F

formal proof, [1]

G

Global aspect GNAT Dynamic Analysis Suite (GNAT DAS), [1], [2], [3] GNATcoverage, [1] GNATemulator, [1] GNATfuzz, [1], [2] GNATtest, [1], [2] TGen, [1] GNAT Dynamic Analysis Suite (GNAT DAS);, [1] GNAT Pro Assurance, [1], [2] Ada language support C language support Configurable Run-Time Libraries, [1] GNAT Pro for Ada GNAT Pro for C GNAT Pro for C++ GNAT Pro for Rust GNATstack Libadalang, [1] Qualification Source-to-object traceability, [1] Support for Annex D techniques (summary) Support for Coding Standards and Style Guide (D.15) Support for Data Flow Analysis (D.10) Support for Defensive Programming (D.14) Sustained branch, [1], [2] GNAT Pro Common Code Generator GNAT Pro Common Code Generator GNAT Pro compiler Exception handling GNAT Pro for Rust, [1], [2] GNAT Static Analysis Suite (GNAT SAS), [1], [2], [3] Defects and Defects and vulnerability analysis, [1] GNATcheck, [1], [2] GNATmetric, [1], [2] Support for Analyzable Programs (D.2) Support for Boundary Value Analysis (D.4) Support for Control Flow Analysis (D.8) Support for Data Flow Analysis (D.10) Support for Defensive Programming (D.14), [1] Support for Impact Analysis (D.32) GNAT Studio IDE, [1], [2] Support for Analyzable Programs (D.2) Support for Control Flow Analysis (D.8) Support for Impact Analysis (D.32) GNATbench

GNATbench IDE, [1] GNATcheck, [1], [2], [3], [4], [5] LKQL (LangKit Query Language) Qualification Support for Analyzable Programs (D.2) Support for Annex D techniques (summary) Support for Coding Standards and Style Guide (D.15) Support for Defensive Programming (D.14) Support for Language Subset (D.35) Support for Modular Approach (D.38), [1] TQL-5 qualification material, [1] GNATcoverage, [1], [2], [3], [4], [5], [6] Data and control coupling coverage Example for Use Case 1a Qualification Source-based instrumentation Support for Annex D techniques (summary) Support for Structure Based Testing (D.50) TQL-5 qualification material, [1] GNATdashboard, [1], [2] GNATdashboard IDE, [1] GNATemulator, [1], [2], [3], [4] Qualification Support for Annex D techniques (summary) Support for Structure Based Testing (D.50) GNATformat, [1] GNATfuzz, [1], [2], [3], [4], [5] Support for Error Guessing (D.20) GNATmetric, [1], [2] Metrics on inter-package coupling Qualification Support for Analyzable Programs (D.2) Support for Annex D techniques (summary) Support for Control Flow Analysis (D.8) Support for Metrics (D.37) GNATprove, [1], [2], [3], [4], [5] GNATstack, [1], [2], [3], [4], [5] Support for Control Flow Analysis (D.8) Tool qualification TQL-5 qualification material, [1] GNATtest, [1], [2], [3], [4], [5], [6], [7] Qualification Support for Annex D techniques (summary) Support for Interface Testing (D.34) Support for Modular Approach (D.38) Support for Structure Based Testing (D.50) GNU GCC technology, [1]

H

High-Level Requirement (HLR)

Hybrid verification, [1], [2]

I

Ichbiah (Jean), [1] integer overflow Integrated Development Environments (IDEs), [1], [2] Eclipse, [1] GNAT Studio, [1], [2] GNATbench, [1] GNATdashboard, [1] VS Code support, [1] Workbench

Integrated Development Environments (IDEs);, [1], [2] interfaces

J

Jorvik profile

Jorvik profile

L

Libadalang, [1] Light Profile, [1], [2] Certification material Level A certification material, [1] Light-Tasking Profile, [1] Certification material Level A certification material, [1]

Liskov Substitution Principle, [1], [2] (LSP) LKQL (LangKit Query Language) Lovelace (Augusta Ada), [1] Low-Level Requirement (LLR)

M

mapping to DO-178C/ED-12C Objectives

mechanism Memory safety, [1]

P

Parameter Data Items, [1] performing resource analysis pessimistic testing PowerPC processor support (by GNAT Pro) pragma Assert Support for Failure Assertion Programming (D.24) pragma Restrictions Support for Coding Standards and Style Guide (D.15) Support for Language Subset (D.35)

Private package Support for Modular Approach (D.38) Project (GNAT Pro) GPR files Support for Modular Approach (D.38)

R

Range checking Ravenscar profile Ravenscar Profile, [1], [2], [3], [4] Support for Language Subset (D.35) Ravenscar profile, [1], [2], [3] Related Techniques Accounting for dispatching in Component-based development Dispatching as a new module coupling Dynamic dispatching Dynamic dispatching and Dynamic memory management Exception handling Exception management Liskov Substitution Principle (LSP) Local and global substitutablity Local type consistency Memory management issues Overloading Overloading and type conversion Parametric polymorphism (genericity) Traceability Type conversion Verifying substitutability by Verifying substitutability through, [1]

Requirement reviews requirement-based testing reviews Robustness / defensive programming, [1] Precondition RTOS support (by GNAT Pro) Rust language support, [1], [2]

S

Safety Integrity Level (SIL), [1] software / software integration tests Software level Software Planning Process Software Quality Assurance Plan source code and object code, [1] SPARK for design data development SPARK language, [1], [2] Absence of Run-Time Errors Absence of run-time errors Alternatives to code coverage when Contributions to architecture Contributions to Low-Level Contributions to Low-Level source Eliminating / reducing testing, [1], [2] Exception handling Formal verification, [1] GNATprove Hybrid verification, [1], [2] Prevention of buffer overrun and Property preservation between, [1] Reduced cost of verification, [1] Robustness Static verification, [1] Support for Language Subset (D.35) Usage, [1] Verifying substitutability through

SPARK Pro toolsuite, [1] GNATprove Qualification SPARK technology Absence of Run-Time Errors (AORTE), [1] Support for Analyzable Programs (D.2) Support for Annex D techniques (summary) Support for Boundary Value Analysis (D.4) Support for Coding Standards and Style Guide (D.15) Support for Data Flow Analysis (D.10) Support for Defensive Programming (D.14), [1] Support for Failure Assertion Programming (D.24) Support for Formal Methods (D.28) Support for Modular Approach (D.38) Specification Structural code coverage Decision Coverage GNATcoverage Modified Condition / Statement Coverage subprogram) substitutability Sustained branch, [1]

T

T1 tool class T2 tool class T3 tool class Taft (Tucker), [1] Techniques, [1] Testing of Outputs of Integration Process TGen, [1], [2], [3] Tool classes Tool qualification, [1] AdaCore support Defects and Vulnerability Analysis GNAT Pro Assurance GNATcheck, [1] GNATcoverage, [1] GNATemulator GNATmetric GNATstack, [1] GNATtest SPARK Pro toolsuite

Traceability of source to object code Analysis for GNAT Pro for Ada and GNAT Pro for C

U

Use Case 1a: Traditional development process, [1], [2], [3], [4], [5], [6], [7], [8], [9], [10] Use Case 1a: Traditional development process excluding OOT Using GNATtest for low-level testing Use Case 1b: Traditional development process including OOT, [1]

Use Case 2: Using SPARK and Formal Methods, [1] Using Use Case 2: Using SPARK and Formal Methods; using proofs

V

V software life cycle, [1], [2], [3] Verification of Outputs of Software Design Process Verification of Verification Process Results

VS Code extensions for Ada and SPARK VS Code support, [1] vulnerabilities vulnerability analysis

W

Workbench

Workbench IDE (Wind River), [1]