5. Summary of contributions to DO-178C/ED-12C objectives
5.1. Overall summary: which objectives are met
The following tables summarize how the Ada and SPARK languages and AdaCore's tools help meet the objectives in DO ‑ 178C/ED ‑ 12C and the technology supplements. The numbers refer to the specific objectives in the core document or the relevant supplement.
Table A-3 and Tables A-8 through A-10 are not included, since they are independent of AdaCore's technologies.
5.1.1. Mapping of AdaCore's Technologies to DO-178C/ED-12C Objectives
|
|
Objectives |
Objectives |
Objectives |
Technology |
Component |
Table A-1 Software Planning Process |
Table A-2 Software Development Process |
Table A-4 Verification of Outputs of Software Design Process |
Programming Language |
Ada |
3, 5 |
3, 4, 5, 6, 7 |
3, 7, 8, 10 |
Programming Language |
SPARK (GNATprove) |
3, 5 |
3, 4, 5, 6, 7 |
FM 14, 15, 16, 17 |
GNAT Pro Toolchain |
GNAT Pro Assurance |
3 |
7 |
|
GNAT Pro Toolchain |
GNATstack |
3, 4 |
|
|
GNAT SAS |
Defects & Vulnerability Analysis |
3, 4 |
|
|
GNAT SAS |
GNATmetric |
3 |
|
|
GNAT SAS |
GNATcheck |
3, 4, 5 |
|
|
GNAT DAS |
GNATtest |
3, 4 |
|
|
GNAT DAS |
GNATemulator |
3 |
|
|
GNAT DAS |
GNATcoverage |
3, 4 |
|
|
IDE |
GPS |
3 |
|
|
IDE |
GNATbench |
3 |
|
|
IDE |
GNATdashboard |
3 |
|
|
|
|
Objectives |
Objectives |
Objectives |
Technology |
Component |
Table A-5 Verification of Outputs of Software Coding and Verification Processes |
Table A-6 Verification of Outputs of Integration Processes |
Table A-7 Verification of Outputs of Verification Process Results |
Programming Language |
Ada |
2, 3, 5, 6, 8, 9 |
|
OO 10, 11 |
Programming Language |
SPARK (GNATprove) |
FM 10, 11, 12, 13 |
3, 4 |
FM 1-10 |
GNAT Pro Toolchain |
GNAT Pro Assurance |
7 |
|
|
GNAT Pro Toolchain |
GNATstack |
6 |
|
|
GNAT SAS |
Defects & Vulnerability Analysis |
3, 4, 6 |
|
|
GNAT SAS |
GNATmetric |
4 |
|
|
GNAT SAS |
GNATcheck |
4 |
|
|
GNAT DAS |
GNATtest |
|
3, 4 |
1, 2 |
GNAT DAS |
GNATemulator |
3, 4 |
|
|
GNAT DAS |
GNATcoverage |
|
|
5, 6, 7, 8 |
IDE |
GPS |
|
|
|
IDE |
GNATbench |
|
|
|
IDE |
GNATdashboard |
|
|
|
5.2. Detailed summary: which activities are supported
In the tables below, the references in the Activities column are to sections in DO ‑ 178C/ED ‑ 12C or to one of the technology supplements. The references in the Use case columns are to sections in this document.
Since AdaCore's tools mostly contribute to the bottom stages of the V cycle (design, coding, integration and related verification activities), verification of High-Level Requirements (and thus Table A-3) are outside the scope of AdaCore solutions.
Likewise, the objectives in Table A-8 (Configuration Management), A-9 (Quality Assurance) and A-10 (Certification Liaison Process) are independent of AdaCore's technologies; they are the responsibility of the user.
5.2.1. Table A-1: Software Planning Process
The objectives of the Software Planning process are satisfied by developing software plans and standards. These activities are the responsibility of the software project. However, using AdaCore solutions can reduce the effort in meeting some of these objectives.
Objective |
Summary |
Activities |
Use case #1a |
Use case #1b (OOT) |
Use case #2 |
1 |
The activities of the software life cycle processes are defined |
All |
This document describes possible methods and tools that may be used. When an AdaCore solution is adopted, it should be documented in the plans. |
Same as #1a |
Same as #1a |
2 |
The software life cycle(s), including the inter-relationships between the processes, their sequencing, and transition criteria, is defined. |
All |
A variety of software life cycles may be defined (such as V cycle, Incremental, Iterative, and Agile). AdaCore solutions do not require any specific software life cycle. |
Same as #1a |
Same as #1a |
3 |
Software life cycle environment is selected and defined |
4.4.1.a, 4.4.1.f, 4.4.2.b, 4.4.3.a, 4.4.3.b |
When an AdaCore solution is used, the plans should identify and escribe the associated tools. In particular, see Sustained Branches and Compiling with the GNAT Pro compiler |
Same as #1a |
Same as #1a |
4 |
Additional considerations are addressed |
4.2.j, 4.2.k |
The need for tool qualification is addressed throughout this document. |
Same as #1a |
Same as #1a |
5 |
Software development standards are defined. |
4.2.b, 4.5.b, 4.5.c, 4.5.d |
This document describes possible languages, methods and tools that may be used during the design and coding processes. When any of them are used, design and code standards must be developed accordingly. A Code Standard can be defined through GNATcheck |
Same as #1a |
Same as #1a |
6 |
Software plans comply with this document. |
All |
This objective is satisfied through the review and analysis of the plans and standards. |
Same as #1a |
Same as #1a |
7 |
Development and revision of software plans are coordinated. |
All |
This objective is satisfied through the review and analysis of the plans and standards. |
Same as #1a |
Same as #1a |
5.2.2. Table A-2: Software Development Processes
AdaCore tools mostly contribute to the bottom stages of the traditional V cycle (design, coding, integration, and the related verification activities).
Objective |
Description |
Activities |
Use case #1a |
Use case #1b (OOT) |
Use case #2 |
1 |
High-level requirements are developed |
5.1.2.j |
Outside the scope of AdaCore solutions, except for Parameter Data Items |
Same as #1a |
Same as #1a |
2 |
Derived high-level requirements are defined and provided to the system processes, including the system safety assessment process. |
|
Outside the scope of AdaCore solutions |
Same as #1a |
Same as #1a |
3 |
Software architecture is developed. |
5.2.2.a |
See Object orientation for the architecture, Memory management issues, Exception handling |
||
4 |
Low-level requirements are developed. |
5.2.2.a |
See Using SPARK for design data development, Robustness and SPARK |
||
5 |
Derived low-level requirements are defined and provided to the system processes, including the system safety assessment process |
5.2.2.b |
See Using SPARK for design data development, Robustness and SPARK |
||
6 |
Source code is developed |
All |
See Benefits of the Ada language, Integration of C components with Ada, Robustness / defensive programming |
Same as #1a |
|
7 |
Executable Object Code and Parameter Data Files, if any produced and loaded in the target computer. |
5.4.2.a, 5.4.2.b, 5.4.2.d |
See Compiling with the GNAT Pro compiler, Integration of C components with Ada, Parameter Data Items |
Same as #1a |
Same as #1a |
5.2.3. Table A-4: Verification of Outputs of Software Design Process
AdaCore solutions may contribute to the verification of the architecture and Low-Level Requirements when Ada/SPARK is used during design process. However, compliance with High-Level Requirements is not addressed by AdaCore solutions.
Objective |
Description |
Activities |
Use case #1a |
Use case #1b (OOT) |
Use case #2 |
1 |
Low-level requirements comply with high-level requirements. |
6.3.2 |
Outside the scope of AdaCore solutions, except for Parameter Data Items |
Same as #1a |
Same as #1a |
2 |
Low-level requirements are accurate and consistent |
6.3.2 |
|
|
|
3 |
Low-level requirements are compatible with target computer. |
6.3.2 |
|
|
|
4 |
Low-level requirements are verifiable. |
6.3.2 |
|
|
|
5 |
Low-level requirements conform to standards. |
6.3.2 |
|
|
|
6 |
Low-level requirements are traceable to high-level requirements. |
|
Outside the scope of AdaCore solutions |
Same as #1a |
Same as #1a |
7 |
Algorithms are accurate. |
6.3.2 |
Same as #1a |
||
8 |
Software architecture is compatible with high-level requirements. |
6.3.3 |
|
|
|
9 |
Software architecture is consistent. |
6.3.3 |
|
|
|
10 |
Software architecture is compatible with target computer. |
6.3.3 |
Same as #1a |
Same as #1a |
|
11 |
Software architecture is verifiable. |
6.3.3 |
|
|
|
12 |
Software architecture conforms to standards. |
6.3.3 |
|
|
|
13 |
Software partitioning integrity is confirmed. |
|
Outside the scope of AdaCore solutions |
Same as #1a |
Same as #1a |
FM14 |
Formal analysis cases and procedures are correct. |
FM 6.3.6 |
|
|
|
FM15 |
Formal analysis results are correct and discrepancies explained. |
FM 6.3.6 |
|
|
|
FM16 |
Requirements formalization is correct. |
FM 6.3.6 |
|
|
|
FM17 |
Formal method is appropriately defined, justified, and appropriate. |
FM 6.3.6 |
|
|
5.2.4. Table A-5 Verification of Outputs of Software Requirement Process
Objective |
Description |
Activities |
Use case #1a |
Use case #1b (OOT) |
Use case #2 |
1 |
Source Code complies with low-level requirements. |
6.3.4 |
|
|
|
2 |
Source Code complies with software architecture. |
6.3.4 |
|
||
3 |
Source Code is verifiable. |
6.3.4 |
|||
4 |
Source Code conforms to standards. |
6.3.4 |
|
||
5 |
Source Code is traceable to low-level requirements. |
6.3.4 |
|
||
6 |
Source Code is accurate and consistent. |
6.3.4 |
See Benefits of the Ada language, Robustness / defensive programming, Checking worst case stack consumption with GNATstack, Checking source code accuracy and consistency with GNAT SAS |
See Benefits of the Ada language, Robustness / defensive programming, Checking worst case stack consumption with GNATstack, Checking source code accuracy and consistency with GNAT SAS, Overloading and type conversion vulnerabilities, Accounting for dispatching in performing resource analysis |
|
7 |
Output of software integration process is complete and correct. |
6.3.5 |
Same as #1a |
Same as #1a |
|
8 |
Parameter Data Item File is complete and correct. |
6.6 |
Same as #1a |
Same as #1a |
|
9 |
Verification of Parameter Data Item File is achieved. |
6.6 |
Same as #1a |
Same as #1a |
|
FM 10 |
Formal analysis cases and procedures are correct. |
FM.6.3.6.a, FM.6.3.6.b |
|
|
|
FM 11 |
Formal analysis results are correct and discrepancies explained. |
FM.6.3.6.c |
|
|
|
FM 12 |
Requirement formalization is correct. |
|
|
||
FM 13 |
Formal method is correctly defined, justified and appropriate. |
FM.6.2.1.a, FM.6.2.1.b, FM.6.2.1.c |
|
|
5.2.5. Table A-6 Testing of Outputs of Integration Process
Objective |
Description |
Activities |
Use case #1a |
Use case #1b (OOT) |
Use case #2 |
1 |
Executable Object Code complies with high-level requirements. |
|
This objective is outside the scope of AdaCore solutions |
Same as #1a |
Same as #1a |
2 |
Executable Object Code is robust with high-level requirements. |
|
This objective is outside the scope of AdaCore solutions |
Same as #1a |
Same as #1a |
3 |
Executable Object Code complies with low-level requirements. |
6.4.2, 6.4.2.1, 6.4.3, 6.5 |
See Using GNATtest for low-level testing, Using GNATemulator for low-level and software / software integration tests |
See Formal analysis as an alternative to low-level testing, Low-level verification by mixing test and proof ("Hybrid verification") |
|
4 |
Executable Object Code is robust with low-level requirements. |
6.4.2, 6.4.2.2, 6.4.3, 6.5 |
See Using GNATtest for low-level testing, Using GNATemulator for low-level and software / software integration tests, Robustness / defensive programming |
Same as #1a |
See Formal analysis as an alternative to low-level testing, Low-level verification by mixing test and proof ("Hybrid verification") |
5 |
Executable Object Code is compatible with target computer. |
|
This objective is based on High-Level Requirements and is thus outside the scope of AdaCore solutions |
Same as #1a |
Same as #1a |
5.2.6. Table A-7 Verification of Verification Process Results
Use case #2 applied formal analysis to verify compliance with Low-Level Requirements. In applying DO ‑ 333/ED ‑ 216, objectives 4 to 7 from DO ‑ 178C/ED ‑ 12C are replaced with objectives FM 1 to FM 10.
Objective |
Description |
Activities |
Use case #1a |
Use case #1b (OOT) |
Use case #2 |
1 |
Test procedures are correct. |
6.4.5 |
Same as #1a |
Limited to verification not performed by formal analysis |
|
2 |
Test results are correct and discrepancies explained. |
6.4.5 |
Same as #1a |
Limited to verification not performed by formal analysis |
|
3 |
Test coverage of high-level requirements is achieved. |
|
This objective concerns the verification of High-Level Requirements and thus is outside the scope of Adacore solutions |
Same as #1a |
Same as #1a |
4 |
Test coverage of low-level requirements is achieved. |
6.4.4.1 |
|
|
|
5 |
Test coverage of software structure (modified condition / decision coverage) is achieved. |
6.4.4.2.a, 6.4.4.2.b |
See Structural code coverage with GNATcoverage, Coverage in the case of generics |
|
|
6 |
Test coverage of software structure (design coverage) is achieved. |
6.4.4.2.a, 6.4.4.2.b |
See Structural code coverage with GNATcoverage, Coverage in the case of generics |
|
|
7 |
Test coverage of software structure (statement coverage) is achieved. |
6.4.4.2.a, 6.4.4.2.b |
See Structural code coverage with GNATcoverage, Coverage in the case of generics |
|
|
8 |
Test coverage of software structure (data coupling and control coupling) is achieved. |
See Data and control coupling coverage with GNATcoverage, Dispatching as a new module coupling mechanism |
|||
9 |
Verification of additional code, that cannot be traced to Source Code, is achieved. |
6.4.4.2.b |
Same as #1a |
Same as #1a |
|
OO 10 |
Verify local type consistency. |
OO.6.7.2 |
|
||
OO 11 |
Verify the use of dynamic memory management is robust. |
OO.6.8.2 |
|
|
|
FM 1 |
Formal analysis cases and procedures are correct. |
|
|
|
|
FM 2 |
Formal analysis results are correct and discrepancies explained. |
|
|
|
|
FM 3 |
Coverage of high-level requirements is achieved. |
|
|
|
In this use case, only LLR are used for formal analysis |
FM 4 |
Coverage of low-level requirements is achieved. |
|
|
|
|
FM 5-8 |
Verification coverage of software structure is achieved. |
FM.6.7.1.2, FM.6.7.1.3, FM.6.7.1.4, FM.6.7.1.5 |
|
|
|
FM 9 |
Verification of additional code, that cannot be traced to Source Code, is achieved. |
FM.6.7 |
|
|
See Property preservation between source code and object code |
FM 10 |
Formal method is appropriately defined, justified and appropriate. |
FM.6.2.1.a, FM.6.2.1.b, FM.6.2.1.c |
|
|
5.3. AdaCore Tool Qualification and Library Certification
Qualification material can be developed for GNATstack and is available for GNATcheck and GNATcoverage:
Tool |
TQL |
DO ‑ 178C/ED ‑ 12C Objectives / Activities |
DO ‑ 330/ED ‑ 215 Objectives / Activities |
GNATstack |
TQL-5 |
A-5[6]: 6.3.4.f |
|
GNATcheck |
TQL-5 |
A-5[4]: 6.3.4.d |
T-5[1..6y]: 6.1.3.4.d |
GNATcoverage |
TQL-5 |
A-7[5..9]: 6.4.4.2 |
T-7[5..9]: 6.1.4.3.2.a |
Certification material up to Software Level A can be developed for the Light and Light-Tasking run-time libraries.