Index

A

Ada language 'Valid attribute Arrays Benefits Concurrent programming Contract-based programming, [1] Dimensionality checking Dynamic dispatching (primitive Endianness Generic templates High-integrity systems History Information hiding Interface / implementation separation, [1] Interfacing with C Memory safety Modulatization Numeric types Object-Oriented Programming (OOP), [1] package Interfaces Packages Pointers Post'Class aspect Postconditions pragma Restrictions Pre'Class aspect Preconditions Prevention of buffer overflow Prevention of dangling references Prevention of null pointer Prevention of vulnerabilities Programming in the large, [1] Real-time programming Scalar ranges Specifying data representation Strong typing, [1] Systems programming

and DO-278A/ED-109A ARM processor support (by GNAT Pro)

B

Bare metal support (by GNAT Pro)

Buffer overflow

C

C language support CENELEC EN 50716:2023 standard Certifiable profile code reviews Code Standard enforcement GNATcheck Common Criteria security standard 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

D

Data and control coupling coverage GNATcoverage Decision Coverage (MC/DC) Defects and vulnerability analysis (in GNAT SAS) dereferencing Design Assurance Level (DAL) 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 Embedded system support (by GNAT Pro) 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] GNATfuzz GNATtest GNAT Dynamic Analysis Suite (GNAT DAS);, [1] GNAT Pro Assurance Ada language support C language support Configurable Run-Time Libraries Libadalang Source-to-object traceability Sustained branch, [1] GNAT Pro Common Code Generator GNAT Pro Common Code Generator GNAT Pro compiler Exception handling GNAT Pro for Rust GNAT Static Analysis Suite (GNAT SAS), [1] Defects and GNATcheck GNATmetric

GNAT Studio IDE GNATbench GNATcheck, [1], [2], [3] LKQL (LangKit Query Language) TQL-5 qualification material, [1] GNATcoverage, [1], [2], [3], [4] Data and control coupling coverage Example for Use Case 1a Source-based instrumentation TQL-5 qualification material, [1] GNATdashboard, [1], [2] GNATemulator, [1], [2] GNATformat GNATfuzz, [1], [2] GNATmetric GNATprove, [1], [2], [3], [4] GNATstack, [1], [2], [3], [4] TQL-5 qualification material, [1] GNATtest, [1], [2], [3], [4] GNU GCC technology, [1]

H

High-Level Requirement (HLR)

Hybrid verification, [1]

I

Ichbiah (Jean) integer overflow Integrated Development Environments (IDEs) Eclipse GNAT Studio

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

J

Jorvik profile

L

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

Liskov Substitution Principle (LSP) LKQL (LangKit Query Language) Lovelace (Augusta Ada) Low-Level Requirement (LLR)

M

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

mechanism Memory safety

P

Parameter Data Items, [1] performing resource analysis

pessimistic testing PowerPC processor support (by GNAT Pro)

R

Ravenscar profile 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

S

software / software integration tests Software level Software Planning Process source code and object code, [1] SPARK for design data development SPARK language, [1] 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 GNATprove Hybrid verification, [1] Prevention of buffer overrun and Property preservation between, [1] Reduced cost of verification Robustness Static verification Usage Verifying substitutability through

SPARK Pro toolsuite Specification Structural code coverage Decision Coverage GNATcoverage Modified Condition / Statement Coverage subprogram) substitutability Sustained branch

T

Taft (Tucker) Techniques, [1] Testing of Outputs of Integration Process TGen, [1] Tool qualification GNATcheck GNATcoverage GNATstack

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] Verification of Outputs of Software Design Process Verification of Verification Process Results

VS Code extensions for Ada and SPARK vulnerabilities vulnerability analysis

W

Workbench

Workbench IDE (Wind River)