4. AdaCore Contributions to the Software Quality Assurance Plan

This chapter identifies AdaCore's tools and technologies that support the techniques and measures defined in the EN 50128 Annex A tables and that can be cited accordingly in the Software Quality Assurance Plan. The information is presented in the form of annotations on the relevant tables in Annex A. These annotations indicate whether a technique or measure is covered by an AdaCore tool or technology and, if so, a comment on how the tool or technology contributes is provided.

Summary of abbreviations:

• M → Mandatory

• HR → Highly Recommended

• R → Recommended

• --- → Optional (neither Recommended nor Not Recommended)

• NR → Not Recommended

4.1. Table A.3 – Software Architecture (7.3)

The Ada language and AdaCore technology do not provide support for software architecture per se, but rather are more targeted towards software component design. However, the presence of some capabilities at the lower level may enable certain design decisions at a higher level. This table offers some guidance on how that can be done.

Technique/Measure	Ref	SIL 2	SIL 3/4	Covered	Comment
Defensive Programming	D.14	HR	HR	Yes	Defensive programming is more a component or a programming activity than an architecture activity per se, but as it is recorded in this table, it's worth mentioning that the Ada language provides several features addressing various objectives of defensive programming techniques (e.g., exception handling). In addition, the GNAT Static Analysis Suite and SPARK tools help identify pieces of code that should be protected by defensive code.
Fault Detection & Diagnosis	D.26	R	R	No
Error Correcting Codes	D.19	—	—	No
Error Detecting Codes	D.19	R	HR	No
Failure Assertion Programming	D.24	R	HR	Yes	The Ada language allows formalizing assertions and contracts in various places in the code.
Safety Bag Techniques	D.47	R	R	No
Diverse Programming	D.16	R	HR	Yes	Using Ada along with another language and a different code generation technology can be used to contribute to the diverse programming argument.
Recovery Block	D.44	R	R	No
Backward Recovery	D.5	NR	NR	No
Forward Recovery	D.30	NR	NR	No
Retry Fault Recovery Mechanisms	D.46	R	R	No
Memorising Executed Cases	D.36	R	HR	No
Artificial Intelligence – Fault Correction	D.1	NR	NR	No
Dynamic Reconfiguration of software	D.17	NR	NR	No
Software Error Effect Analysis	D.25	R	HR	No
Graceful Degradation	D.31	R	HR	No
Information Hiding / Encapsulation	D.33	HR	HR	Yes	The Ada language provides the necessary features to separate the interface of a module from its implementation and enforce this separation.
Fully Defined Interface	D.38	HR	M	Yes	The Ada language provides the necessary features to separate the interface of a module from its implementation and enforce this separation.
Formal Methods	D.28	R	HR	Yes	SPARK can be used to formally define architectural properties, such as data flow, directly in the code and provides the means to verify them.
Modeling	Table A.17	R	HR	Yes	Ada and SPARK allow defining certain modeling properties in the code and provide means to verify them.
Structured Methodology	D.52	HR	HR	Yes	Structured Methodology designs can be implemented with Ada.
Modeling supported by computer aided design and specification tools	Table A.17	R	HR	No

4.2. Table A.4 – Software Design and Implementation (7.4)

Technique/Measure	Ref	SIL 2	SIL 3/4	Covered	Comment
Formal Methods	D.28	R	HR	Yes	Component requirements and interfaces can be written in the form of formal boolean properties, using the Ada or SPARK languages. These properties are verifiable.
Modeling	Table A.17	HR	HR	Yes	Ada and SPARK allow defining certain modeling properties in the code and provide means to verify them.
Structured methodology	D.52	HR	HR	Yes	Structured Methodology designs can be implemented with Ada.
Modular Approach	D.38	M	M	Yes	A module can be represented as an Ada package, with a cohesive and well-defined functionality, a clear external interface in the visible part of the package spec, a private part whose visibility is limited to to its child units, and a body containing the implementation (which is only visible to its subunits).
Components	Table A.20	HR	HR	Yes	A component can be defined as a set of Ada packages, which can clearly define the interface to access the internal data, and the interfaces can be fully and unambiguously defined. This set of packages is typically identified within a project file (GPR file) and can be put into a version control system.
Design and Coding Standards	Table A.12	HR	M	Yes	There are available references for the coding standard. Verification can be automated in different ways: the GNAT compiler can define base coding standard rules to be checked at compile-time, with GNATcheck implementing a wider range of rules.
Analyzable Programs	D.2	HR	HR	Yes	The Ada language provide native features to improve program analysis, such as type ranges, parameter modes, and encapsulation. Tools such as GNATmetric and GNATcheck can help monitor the complexity of the code and prevent the use of overly complex code. GNAT SAS allows making an assessment of program analyzability during its development. For higher SILs, the use of SPARK ensures that the subset of the language used is suitable for most the rigorous analysis.
Strongly Typed Programming Language	D.49	HR	HR	Yes	Ada is a strongly typed language.
Structured Programming	D.53	HR	HR	Yes	Ada supports all the usual paradigms of structured programming. In addition, GNATcheck can control additional design properties, such as explicit control flows, where subprograms have single entry and single exit points, and structural complexity is reduced.
Programming Language	Table A.15	HR	HR	Yes	Ada can be used for most of the development, while facilitating interfacing to other languages such as C or assembly.
Language Subset	D.35	—	HR	Yes	Ada is designed to support subsetting, possibly under the control of specific runtimes, GNATcheck, or with SPARK. Another possibility is to follow the recommendations in [ISOIECJTC1SC2298].
Object-Oriented Programming	Table A.22, D.57	R	R	Yes	If needed, Ada supports all the usual paradigms of object-oriented programming, in addition to safety-related features such as the Liskov Substitution Principle.
Procedural Programming	D.60	HR	HR	Yes	Ada supports all the usual paradigms of procedural programming.
Metaprogramming	D.59	R	R	No

4.3. Table A.5 – Verification and Testing (6.2 and 7.3)

Technique/Measure	Ref	SIL 2	SIL 3/4	Covered	Comment
Formal Proof	D.29	R	HR	Yes	When Ada pre- and post-conditions are used, together with the SPARK subset of the language, formal methods can formally verify compliance of the implementation with these contracts.
Static Analysis	Table A.19	HR	HR	Yes	See Table A.19
Dynamic Analysis and Testing	Table A.13	HR	HR	Yes	See Table A.13
Metrics	D.37	R	R	Yes	GNATmetric can compute and report metrics, such as code size, comment percentage, cyclomatic complexity, unit nesting, and loop nesting. These can then be compared with standards.
Traceability	D.58	HR	M	No
Software Error Effect Analysis	D.25	R	HR	Yes	GNAT Studio supports code display and navigation. GNAT SAS can identify likely error locations in the code. This supports potential software error detection and analysis throughout the code.
Test Coverage for code	Table A.21	HR	HR	Yes	See Table A.21
Functional / Black-Box Testing	Table A.14	HR	HR	Yes	See Table A.14
Performance Testing	Table A.18	HR	HR	No
Interface Testing	D.34	HR	HR	Yes	Ada's strong typing, together with its contract-based programming support, provides increased assurance to demonstrate that the software interfaces are correct. This can help improve software-to-software integration testing.

4.4. Table A.6 – Integration (7.6)

Technique/Measure	Ref	SIL 2	SIL 3/4	Covered	Comment
Functional and Black-box testing	Table A.14	HR	HR	Yes	GNATtest can generate a framework for testing.
Performance Testing	Table A.18	R	HR	Yes	Stack consumption can be statically computed using the GNATstack tool.

4.5. Table A.7 – Overall Software Testing (6.2 and 7.7)

Technique/Measure	Ref	SIL 2	SIL 3/4	Covered	Comment
Performance Testing	Table A.18	HR	M	Yes	Stack consumption can be statically computed using the GNATstack tool.
Functional and Black-box Testing	Table A.14	HR	M	Yes	GNATtest can generate a testing framework for testing.
Modeling	Table A.17	R	R	No

4.6. Table A.8 – Software Analysis Techniques (6.3)

Technique/Measure	Ref	SIL 2	SIL 3/4	Covered	Comment
Static Software Analysis	D.13, D.37, Table A.19	HR	HR	Yes	See Table A.19.
Dynamic Software Analysis	Tables A.13, A.14	R	HR	Yes	See Tables A.13 and A.14.
Cause Consequence Diagrams	D.6	R	R	No
Event Tree Analysis	D.22	R	R	No
Software Error Effect Analysis	D.25	R	HR	Yes	GNAT Studio supports code display and navigation. GNAT SAS can identify likely error locations in the code. These tools support both detection of potential software errors and analysis throughout the code.

4.7. Table A.9 – Software Quality Assurance (6.5)

Although AdaCore doesn't directly provide services for ISO 9001 or configuration management, it follows standards to enable tool qualification and/or certification. The following table only lists items that can be useful to third parties.

Technique/Measure	Ref	SIL 2	SIL 3/4	Covered	Comment
Accredited to EN ISO 9001	7.1	HR	HR	No
Compliant with EN ISO 9001	7.1	M	M	No
Compliant with ISO/IEC 90003	7.1	R	R	No
Company Quality System	7.1	M	M	No
Software Configuration Management	D.48	M	M	No
Checklists	D.7	HR	M	No
Traceability	D.58	HR	M	No
Data Recording and Analysis	D.12	HR	M	Yes	The data produced by tools can be written to files and placed under configuration management.

4.8. Table A.10 – Software Maintenance (9.2)

Technique/Measure	Ref	SIL 2	SIL 3/4	Covered	Comment
Impact Analysis	D.32	HR	M	Yes	GNAT SAS contributes to identifying the impact of a code change between two baselines.
Data Recording and Analysis	D.12	HR	M	Yes	AdaCore tools can be invoked from the command line. They produce result files including the date and version of the tool used.

4.9. Table A.11 – Data Preparation Techniques (8.4)

Technique/Measure	Ref	SIL 2	SIL 3/4	Covered	Comment
Tabular Specification Methods	D.68	R	R	Yes	Tables of data can be expressed using the Ada language, together with type-wide contracts (predicates or invariants).
Application specific language	D.69	R	R	No
Simulation	D.42	HR	HR	No
Functional testing	D.42	M	M	No
Checklists	D.7	HR	M	No
Fagan inspection	D.23	HR	HR	No
Formal design reviews	D.56	HR	HR	Yes	GNAT Studio can display code and navigate through the code as a support for walkthrough activities.
Formal proof of correctness	D.29	—	HR	Yes	When contracts are expressed within the SPARK subset, their correctness can be formally verified.
Walkthrough	D.56	R	HR	Yes	GNAT Studio can display code and navigate through the code as a support for walkthrough activities.

4.10. Table A.12 – Coding Standards

There are available references for coding standards. Their verification can be automated through different ways: the GNAT compiler can define base coding standard rules to be checked at compile time, and GNATcheck implements a wider range of rules and is tailorable to support project-specific coding standards.

Technique/Measure	Ref	SIL 2	SIL 3/4	Covered	Comment
Coding Standard	D.15	HR	M	Yes	GNATcheck allows implementing and verifying a coding standard.
Coding Style Guide	D.15	HR	HR	Yes	GNATcheck allows implementing and verifying a coding style guide.
No Dynamic Objects	D.15	R	HR	Yes	GNATcheck can forbid the use of dynamic objects.
No Dynamic Variables	D.15	R	HR	Yes	GNATcheck can forbid the use of dynamic variables.
Limited Use of Pointers	D.15	R	R	Yes	GNATcheck can forbid the use of pointers or force justification of their usage.
Limited Use of Recursion	D.15	R	HR	Yes	GNATcheck can forbid the use of recursion or force justification of their usage.
No Unconditional Jumps	D.15	HR	HR	Yes	GNATcheck can forbid the use of unconditional jumps.
Limited size and complexity of Functions, Subroutines and Methods	D.38	HR	HR	Yes	GNATmetric can compute complexity measures, and GNATcheck can report excessive complexity.
Entry/Exit Point strategy for Functions, Subroutines and Methods	D.38	HR	HR	Yes	GNATcheck can verify rules related to exit points.
Limited number of subroutine parameters	D.38	R	R	Yes	GNATcheck can limit the number of parameters for subroutines and report when that number is exceeded.
Limited use of Global Variables	D.38	HR	M	Yes	GNATcheck can flag global variable usage and enforce their justification. SPARK forbids function side effects and enforces documentation and verification of uses of global variables. GNAT Studio allows analyzing usage of global variables.

4.11. Table A.13 – Dynamic Analysis and Testing

Technique/Measure	Ref	SIL 2	SIL 3/4	Covered	Comment
Test Case Execution from Boundary Value Analysis	D.4	HR	HR	Yes	GNATtest can generate and execute a testing framework for tests written by developers from requirements.
Test Case Execution from Error Guessing	D.20	R	HR	Yes	GNAT fuzz can automate the generation of large numbers of test cases at a high frequency.
Test Case Execution from Error Seeding	D.21	R	HR	No
Performance Modeling	D.39	R	HR	No
Equivalence Classes and Input Partition Testing	D.18	R	HR	Yes	Ada and SPARK provide specific features for partitioning function input and verifying that this partitioning is well formed (i.e., no overlap and no gaps).
Structure-Base Testing	D.50	R	HR	Yes	See Table A.21

4.12. Table A.14 – Functional/Black Box Test

GNATtest can generate and execute a testing framework, with the actual tests being written by developers from requirements.

Technique/Measure	Ref	SIL 2	SIL 3/4	Covered	Comment
Test Case Execution from Cause Consequence Diagrams	D6	—	R	No
Prototyping/ Animation	D.43	—	R	No
Boundary Value Analysis	D.4	R	HR	Yes	GNATtest can be used to implement tests coming from boundary value analysis.
Equivalence Classes and Input Partitioning Testing	D.18	R	HR	Yes	Ada and SPARK provide specific features for partitioning function input and verifying that this partitioning is well formed (i.e., no overlap and no gaps).
Process Simulation	D.42 R	R	No

4.13. Table A.15 – Textual Programming Language

Technique/Measure	SIL 2	SIL 3/4	Covered	Comment
Ada	HR	HR	Yes	GNAT Pro tools support all versions of the Ada language.
MODULA-2	HR	HR	No
PASCAL	HR	HR	No
C or C++	R	R	Yes	GNAT Pro for C and GNAT Pro for C++ support these languages
PL/M	R	NR	No
BASIC	NR	NR	No
Assembler	R	R	No
C#	R	R	No
Java	R	R	No
Statement List	R	R	No

4.14. Table A.17 – Modeling

Technique/Measure	Ref	SIL 2	SIL 3/4	Covered	Comment
Data Modeling	D.65	R	HR	Yes	Ada allows modeling data constraints, in the form of type predicates.
Data Flow Diagram	D.11	R	HR	Yes	SPARK allows defining data flow dependencies at subprogram specification.
Control Flow Diagram	D.66	R	HR	No
Finite State Machine or State Transition Programs	D.27	HR	HR	No
Time Petri Nets	D.55	R	HR	No
Decision/Truth Tables	D.13	R	HR	No
Formal Methods	D.28	R	HR	Yes	SPARK allows defining formal properties on the code that can be verified by the SPARK toolset.
Performance Modeling	D.39	R	HR	No
Prototyping/Animation	D.43	R	R	No
Structure Diagrams	D.51	R	HR	No
Sequence Diagrams	D.67	R	HR	No

4.15. Table A.18 – Performance Testing

Technique/Measure	Ref	SIL 2	SIL 3/4	Covered	Comment
Avalanche/Stress Testing	D.3	R	HR	No	Ada allows modeling data constraints, in the form of type predicates.
Response Timing and Memory Constraints	D.45	HR	HR	Yes	GNATstack can statically analyze stack usage.
Performance Requirements	D.40	HR	HR	No

4.16. Table A.19 – Static Analysis

Technique/Measure	Ref	SIL 2	SIL 3/4	Covered	Comment
Boundary Value Analysis	D.4	R	HR	Yes	GNAT SAS can compute boundary values for variables and parameters from the source code. GNAT SAS and SPARK can verify various properties by analyzing potential values and boundary values of variables. This includes detecting errors such as dereferencing a pointer that could be null, generating a value outside the bounds of an Ada type or subtype, violating a memory safety constraint (buffer overrun), generating a numeric overflow or wraparound, and dividing by zero. GNAT SAS and SPARK also help to confirm expected boundary values of variables and parameters coming from the design.
Checklists	D.7	R	R	No
Control Flow Analysis	D.8	HR	HR	Yes	GNAT SAS and SPARK can detect suspicious and potentially incorrect control flows, such as unreachable code, redundant conditionals, loops that either run forever or fail to terminate normally, and subprograms that never return. GNATstack can analyze control flow and compute the maximum amount of stack memory for each task. More generally, GNAT Studio provides visualization for call graphs and call trees.
Data Flow Analysis	D.10	HR	HR	Yes	GNAT SAS and SPARK can detect suspicious and potentially incorrect data flow, such as variables being read before they are written (uninitialized variables), and values that are written to variables without being read (redundant assignments).
Error Guessing	D.20	R	R	Yes	Although realized through dynamic rather than static analysis, GNAT fuzz can automatically generate test cases to support Error Guessing.
Walkthroughs/Design Reviews	D.56	HR	HR	Yes	GNAT Studio can display and navigate the code, supporting walkthrough activities.

4.17. Table A.20 – Components

Technique/Measure	Ref	SIL 2	SIL 3/4	Covered	Comment
Information Hiding	D.33	—	—	Yes	See Information Encapsulation below.
Information Encapsulation	D.33	HR	HR	Yes	Ada provides the necessary features to separate the interface of a module from its implementation, and enforce this separation.
Parameter Number Limit	D.38	R	R	Yes	GNATcheck can limit the number of parameters for subroutines, and report violations.
Fully Defined Interface	D.38	HR	M	Yes	Ada offers many features to support interface definition, including behavior specification through pre- and post-conditions.

4.18. Table A.21 – Test Coverage for Code

Technique/Measure	Ref	SIL 2	SIL 3/4	Covered	Comment
Statement	D.50	HR	HR	Yes	GNATcoverage provides statement-level coverage capabilities.
Branch	D.50	R	HR	Yes	GNATcoverage provides branch-level coverage capabilities.
Compound Condition	D.50	R	HR	Yes	GNATcoverage provides MC/DC (Modified Condition/Decision Coverage) capabilities, which can be used as an efficient alternative to Compound Condition coverage.
Data Flow	D.50	R	HR	No
Path	D.50	R	NR	No

4.19. Table A.22 – Object Oriented Software Architecture

Technique/Measure	Ref	SIL 2	SIL 3/4	Covered	Comment
Traceability of the concept of the application domain to the classes of the architecture	—	R	HR	No
Use of suitable frames, commonly used combinations of classes and design patterns	—	R	HR	Yes	The conventional OO design patterns can be implemented in Ada.
Object Oriented Detailed Design	Table A.23	R	HR	Yes	See Table A.23

4.20. Table A.23 – Object Oriented Detailed Design

Technique/Measure	Ref	SIL 2	SIL 3/4	Covered	Comment
Class should have only one objective	—	R	HR	Yes	It's possible in Ada to write classes with a unique objective.
Inheritance used only if the derived class is a refinement of its basic class	—	HR	HR	Yes	Ada and SPARK can enforce respecting the Liskov Substitution Principle, ensuring inheritance consistency.
Depth of inheritance limited by coding standards	—	R	HR	Yes	GNATcheck can limit inheritance depth.
Overriding of operations (methods) under strict control	—	R	HR	Yes	Ada can enforce explicit syntax for overriding methods.
Multiple inheritance used only for interface classes	—	HR	HR	Yes	Ada only allows multiple inheritance from interfaces.
Inheritance from unknown classes	—	—	NR	Yes	Ada only allows inheritance from known classes.

Bibliography