11. Traceability to ISO 26262

This chapter identifies the ISO 26262 objectives, requirements, and recommendations that are achieved (or complied with) through following the process defined in NVIDIA SPARK Process, for those software units developed according to this process. This section also identifies which process steps support each of the ISO 26262 objectives, requirements, and recommendations, and why the process steps are sufficient.

This chapter is grouped into sections based on the clause of ISO 26262 being addressed.

Each row of each table below shall be understood as follows: If the development team faithfully follows the process step(s) / section(s) listed in the second column, then the resulting work product(s) will comply with the objective, requirement, or recommendation in the first column, because of the argument provided in the third column. Each argument must be derived only from the listed process step(s) / section(s).

11.1. Attribution

Any material from the ISO standards (anything typeset in boxes or referencing a part and section) is subject to the following notice:

(C)ISO. This material is reproduced from ISO 26262, with permission of the American National Standards Institute (ANSI) on behalf of the International Organization for Standardization. All rights reserved.

The text in this chapter is generated from TRLC files - and this attribution therefore also applies to the fields text, row, and applies for the type Tracing.

11.2. List of Objectives, Requirements, and Recommendations in ISO 26262 Fully Met By Following This Process

The process fully addresses the objectives, requirements, and recommendation in ISO 26262 in the following causes:

• Part 6, Clause 5 “General topics for the product development at the software level”, to the extent it relates to software unit level work products for software units developed according to this process

• Part 6, Clause 6 “Specification of software safety requirements”

• Part 6, Clause 8 “Software unit design and implementation” for software units developed according to this process

• Part 6, Clause 9 “Software unit verification” for software units developed according to this process

• Part 8, Clause 6 “Specification and management of safety requirements”, to the extent it concerns safety requirements at the software unit level for software units developed according to this process

• Part 8, Clause 9 “Verification”, as instantiated for:

  • Part 6, Clause 6: Specification of software safety requirements

  • Part 6, Clause 8: Software unit design and implementation

11.3. Notation in the ISO 26262 Traceability Tables

In traceability table rows corresponding to ISO 26262 Table rows, the letters within square brackets ([]) indicate the ASILs at which the table row is recommended (lower-case) or highly recommended (upper-case). For example, [abCD] indicates a table row that is recommended for ASILs A and B, and highly recommended for ASILs C and D. As another example, [Ab] indicates a table row that is highly recommended for ASIL A, recommended for ASIL B, and not recommended for ASILs C and D.

In some rows, the first column cites some text from ISO 26262 but the other columns are grayed out. This indicates that the text from ISO 26262 is introductory and is fully addressed by the subsequent rows.

11.4. ISO 26262-6:2018, Clause 5: General topics for the product development at the software level

11.4.1. Section 5.1

Part 6 - Section 5.1:

The objectives of this clause are:

1. to ensure a suitable and consistent software development process; and

2. to ensure a suitable software development environment.

Process steps that apply: N/A

Justification:

These objectives are fully covered through the requirements and recommendations in 6-5.4, all enumerated below. Note however that not all of the requirements and recommendations are applicable to software unit requirements, design, implementation, and verification, and thus not all are applicable to this process.

11.4.2. Section 5.4

Part 6 - Section 5.4.1 a:

When developing the software of an item, software development processes and software development environments shall be used which:

1. are suitable for developing safety-related embedded software, including methods, …

Process steps that apply: (All)

Justification:

The software development methods prescribed by this process, embodied in the process steps, are suitable for developing safety-related embedded software because these methods were developed based on a systematic consideration of the objectives, requirements, and recommendations of ISO 26262.

Part 6 - Section 5.4.1 a:

…, guidelines, …

Process steps that apply: (Various)

Justification:

Guidelines are used to improve the comprehensibility and consistency of the work products and to identify and avoid known pitfalls. Specific guidelines documents are cited along with their corresponding process step IDs as needed. For a complete list of guideline documents, see section entitled “Ada/SPARK Guidelines”.

Part 6 - Section 5.4.1 a:

…, languages …

Process steps that apply: (All)

Justification:

The Ada language is suitable for developing safety-related embedded software.

The Ada language has been designed to be easily subsettable. In its core definition, it defines a series of restrictions that can be applied, deactivating certain features of the language. GNAT run-times, such as the so-called light (no run-time component) or light-tasking provide other natural subsets to the language, which have direct implications in terms of portability, determinism or even safety.

SPARK is an Ada language subset, constraining the language in a more analyzable subset (for example, no aliasing, and no exceptions).

SPARK is suitable to specify software requirements: it is a formal notation with fully specified syntax and semantics, which enables creation of unambiguous and verifiable requirements specifications

If software requirements are specified in SPARK and a unit is implemented in SPARK, the consistency of implementation and requirements is formally proven with GNATprove.

Part 6 - Section 5.4.1 a:

… and tools;

Process steps that apply: (Various)

Justification:

Tools are employed throughout this process. Each of the prescribed Ada tools is analyzed to determine a TCL, and, for TCL2 and TCL3, qualified by AdaCore for the development of ASIL D embedded software. See section entitled “Software Tool Usage Analysis” for the determination of TCLs.

Part 6 - Section 5.4.1 b:

b) support consistency across the sub-phases of the software development lifecycle and the respective work products; and

Process steps that apply:

• Verify_Requirement_Correctness_And_Completeness

• Inspect_Unit_Design

• Verify_Project

• Automated_Check_Against_Coding_Std

• Inspect_Implementation

Justification:

Consistency of the software development life cycle is ensured through the practices prescribed throughout this document.

Consistency of the respective work products is ensured through the steps enumerated above.

Part 6 - Section 5.4.1 c:

c) are compatible with the system and hardware development phases regarding required interaction and consistency of exchange of information.

Process steps that apply: Declare_Types_States_And_Subprograms

Justification:

In Ada, it is possible to specify representation aspects in order to interface with features that are outside the domain of the language, typically the hardware.

Part 6 - Section 5.4.2 a:

The criteria that shall be considered when selecting a design, modelling or programming language are:

1. an unambiguous and comprehensible definition;

Process steps that apply: N/A

Justification:

Ada is defined by its ISO standard, aka the Ada Reference Manual, the latest version being ISO/IEC 8652:2012 defining version 2012 of the language.

SPARK is a software development technology specifically designed for engineering high-reliability applications. It is defined through a document called the SPARK Reference Manual which follows the structure and style of the Ada Reference Manual.

Part 6 - Section 5.4.2 b:

b) suitability for specifying and managing safety requirements according to ISO 26262-8:2018 Clause 6, if modelling is used for requirements engineering and management;

Process steps that apply:

• Capture_Requirements

• Assign_Requirement_Unique_IDs

Justification:

SPARK contracts are used to specify safety requirements. See section entitled “ISO 26262-8:2018, Clause 6: Specification and management of safety requirements” for details

Part 6 - Section 5.4.2 c:

c) support the achievement of modularity, abstraction and encapsulation; and

Process steps that apply:

• Identify_Activity_Scope

• Capture_Requirements

• Implement_SPARK_Package

• Verify_Project

Justification:

By following the process above, a module is represented as an Ada package, with a well-defined functionality, a clear software interface in the package specification, a private part to limit the visibility only to child packages, and a body containing the implementation which is not visible to any other module.

Since Ada 83, Ada has been object-based, allowing the partitioning of a system into modules corresponding to abstract data types or abstract objects.

Ada provides the necessary features to separate the software interface of a module from its implementation, and enforce respect of this separation.

A package in SPARK is fully responsible for modifications of its internal data (including data of local packages or private child packages) that it only exposes to client packages through abstract names (called “abstract state”). In particular, package elaboration code executed at program startup only directly initializes the data of the package itself.

Type invariants in SPARK are suitably restricted so that a package ensures that all objects of the type respect their invariant outside of the package boundary.

Formal verification in SPARK is performed modularly on each package separately.

Part 6 - Section 5.4.2 d:

4. support the use of structured constructs.

Process steps that apply: Automated_Check_Against_Coding_Std

Justification:

Ada supports all the usual paradigms of structured programming. In addition to these, GNATcheck controls additional design properties, such as explicit control flows, where subprograms have single entry and single exit points, and if structural complexity is too high.

Part 6 - Section 5.4.3 Table 1, 1a:

Criteria for suitable modelling, design or programming languages (see 5.4.2) that are not sufficiently addressed by the language itself shall be covered by the corresponding guidelines, or by the development environment, considering the topics listed in Table 1.

	A	B	C	D
Enforcement of low complexity	++	++	++	++

An appropriate compromise of this topic with other requirements of this document may be required

Process steps that apply:

• Verify_Project

• Automated_Check_Against_Coding_Std

• Fix_Coding_Std_Issues

• Review_Diagnostic_Justifications

Justification:

The Automated Check Against Coding Standard and Safety Manual step requires the use of GNATcheck in accordance with the Requirements Concerning GNATcheck Switches and Rules section. One of the rules required by this process for non-proven Ada code is Metrics_Cyclomatic_Complexity:10, which (when restricted to non-proven code via GNATcheck) results in a GNATcheck diagnostic for each non-proven subprogram whose McCabe cyclomatic complexity exceeds 10.

The Fix Coding Standard and Safety Manual Violations step requires for each excessively-complex non-proven subprogram that either the subprogram is simplified or (where an appropriate compromise is necessary, as allowed by ISO 26262) a rationale is provided for the complexity via a diagnostic justification that is later review din the Review Diagnostic Justifications step.

Proven subprograms are exempted from this evaluation because the risk associated with excessive complexity is sufficiently mitigated by the use of GNATprove in the Verify Project step, which always verifies the absence of run-time errors in proven code.

Part 6 - Section 5.4.3 Table 1, 1b:

	A	B	C	D
Use of language subsets	++	++	++	++

The objectives of topic 1b include:

• Exclusion of ambiguously-defined language constructs which may be interpreted differently by different modellers programmers, code generators or compilers.

• Exclusion of language constructs which from experience easily lead to mistakes, for example assignments i conditions or identical naming of local and global variables.

• Exclusion of language constructs which could result in unhandled run-time errors.

Process steps that apply:

• Implement_SPARK_Package

• Verify_Project

• Review_Deactivated_SPARK

• Create_Project_File

• Automated_Check_Against_Coding_Std

• Fix_Coding_Std_Issues

• Automated_Check_Against_Coding_Std_Integration

Justification:

The Ada language was designed to mitigate the kinds of threats identified in the footnote for 1b). For example, statements and expressions are linguistically separate, and consequently an assignment (a kind of statement) cannot appear within a condition (a kind of expression). Furthermore, assignments employ a symbol (:=) that is not easily confused with a comparison operator. These sorts of language design features permeate Ada making language subsetting less critical than with more general-purpose languages like C and C++.

The language SPARK is a language subset of Ada designed to facilitate sound static verification by restricting use of access types, function side effects, aliasing, goto’s, controlled types, and exceptions. This subsetting is enabled with SPARK_Mode => On (see Implement SPARK Package step). When enabled, GNATprove verifies the absence of run-time errors (see Verify Project step). When not enabled, additional global peer review is triggered (see Review Deactivated SPARK step).

Finally, automated enforcement of language subsetting for both Ada and SPARK is achieved using GNATcheck (see Create Project File, Automated Check Against Coding Standard and Safety Manual, Fix Coding Standard and Safety Manual Violations, and GNATcheck and gnatkp on whole program steps).

Part 6 - Section 5.4.3 Table 1, 1c:

	A	B	C	D
Enforcement of strong typing	++	++	++	++

The objective of topic 1c is to impose principles of strong typing where these are not inherent in the language.

Process steps that apply: N/A

Justification:

Strong typing is a native feature of the Ada language.

Part 6 - Section 5.4.3 Table 1, 1d:

	A	B	C	D
Use of defensive implementation techniques	+	+	++	++

Examples of defensive implementation techniques

• Verify the divisor before a division operation (different from zero or in a specific range).

• Check an identifier passed by parameter to verify that the calling function is the intended caller.

• Use the “default” in switch cases to detect an error.

Process steps that apply:

• Implement_SPARK_Package

• Verify_Project

• Review_Deactivated_SPARK

Justification:

In most cases, defensive techniques are not required because Ada/SPARK has built in support for them.

For example, Ada requires the use of others in a case statement when all possible inputs are not otherwise covered (C calls these default and switch, respectively).

For SPARK code, GNATprove verifies the Absence of Run-time Errors (AoRTE), as well as correctness of SPARK contracts.

For deactivated SPARK code, the process requires the presence of language-defined runtime checks to dynamically ensure that SPARK contracts are fulfilled.

If it is necessary to disable such runtime checks, then the process asks for using defensive implementation techniques to mitigate the risk associated with absence of the contract checks.

Part 6 - Section 5.4.3 Table 1, 1e:

	A	B	C	D
Use of well-trusted design principles	+	+	++	++

Verification of the validity of the underlying assumptions, boundaries and conditions of application may be required.

Process steps that apply:

• Identify_Activity_Scope

• Capture_Requirements

• Implement_SPARK_Package

Justification:

Ada and SPARK support well-trusted design principles:

• structured control statements;

• flexible data composition facilities, with strong type checking;

• traditional features for code modularization (“subprograms”);

• standard support for “programming in the large” and module reuse (packages, Object-Oriented Programming, child libraries, generic templates);

• a mechanism for detecting and responding to exceptional run-time conditions (“exception handling”);

• high-level concurrency support (“tasking”) along with a deterministic subset (the Ravenscar profile) appropriate in applications that need to meet high-assurance certification requirements.

The Ada/SPARK Guidelines identify well-trusted design principles, and the process requires that these guidelines be considered when reviewing Ada/SPARK code.

Part 6 - Section 5.4.3 Table 1, 1f:

	A	B	C	D
Use of unambiguous graphical representation	+	++	++	++

Process steps that apply: N/A

Justification:

Not covered.

Part 6 - Section 5.4.3 Table 1, 1g:

	A	B	C	D
Use of style guides	+	++	++	++

Process steps that apply:

• Verify_Requirement_Correctness_And_Completeness

• Inspect_Unit_Design

• Automated_Check_Against_Coding_Std

• Inspect_Implementation

Justification:

GNATcheck is used to automate enforcement of the Ada/SPARK Guidelines employed by this process.

Aspects of the Ada/SPARK Guidelines that are not enforced by GNATcheck are verified by manual inspection.

Part 6 - Section 5.4.3 Table 1, 1h:

	A	B	C	D
Use of naming conventions	++	++	++	++

Process steps that apply:

• Automated_Check_Against_Coding_Std

• Fix_Coding_Std_Issues

• Create_Project_File

Justification:

GNATcheck is used to automate enforcement of the Ada/SPARK Guidelines employed by this process.

Naming conventions are the purview of these guidelines.

Also, the GNAT naming conventions for files are adopted. The Create Project File forbids project files from including Naming packages.

Part 6 - Section 5.4.3 Table 1, 1i:

	A	B	C	D
Concurrency aspects	+	+	+	+

Concurrency of processes or tasks is not limited to executing software in a multi-core or multi-processor runtime environment.

Process steps that apply:

• Inspect_Unit_Design

• Automated_Check_Against_Coding_Std

• Inspect_Implementation

Justification:

Assurance of the suitability and consistency of the software development process with respect to concurrency is the purview of the Ada/SPARK Guidelines. These guidelines are enforced through automation via GNATcheck and through manual inspections.

Assurance of the suitability of the software development environment is addressed by Ada/SPARK and is not limited to any set of process steps.

Ada supplies a structured, high-level facility for concurrency. The unit of concurrency is a program entity known as a “task.” Tasks typically communicate implicitly via shared data or explicitly via a synchronous control mechanism known as the rendezvous. A shared data item is defined abstractly as a “protected object” (a feature introduced in Ada 95), with operations executed under mutual exclusion when invoked from multiple tasks. Asynchronous task interactions are also supported, specifically timeouts and task termination. Such asynchronous behavior is deferred during certain operations, to prevent the possibility of leaving shared data in an inconsistent state. Mechanisms designed to help take advantage of multi-core architectures that were introduced in Ada 2012. In Ada, light-tasking runtime supports this concurrency mode.

SPARK also supports light-tasking runtime.

11.4.3. Section 5.5

Part 6 - Section 5.5.1:

Work products

Documentation of the software development environment resulting from requirements 5.4.1 to 5.4.3 and C.4.1 to C.4.11.

Process steps that apply:

See this section and sections entitled: “Ada/SPARK Guidelines”, “Software Tool Usage Analysis”

Justification:

• Ada/SPARK Guidelines are described in a separate document. See section entitled “Ada/SPARK Guidelines”

• Tools are documented in section “Software Tool Usage Analysis”

• Configuration and calibration data are outside the scope of this process.

11.5. ISO 26262-6:2018, Clause 6: Specification of software safety requirements

Note: This clause is applicable to this process because this process allows software safety requirements at the software unit level to be expressed in ADS files. However, much of the content of ISO 26262-6:2018, Clause 6 is relevant only to software safety requirements at the level of the embedded software as a whole, which is outside the scope of this process. Where objectives, requirements, or recommendations of ISO 26262-6:2018, Clause 6 are not relevant to software safety requirements at the software unit level, the corresponding section indicates as much and does not trace to any process steps.

11.5.1. Section 6.1

Part 6 - Section 6.1 a:

The objectives of this sub-phase are:

1. to specify or refine the software safety requirements which are derived from the technical safety concept and the system architectural design specification;

Process steps that apply: N/A

Justification:

Out of scope: Software safety requirements for software components below the level of embedded software are not derived from the TSC or the system architectural design specification, but rather from software safety requirements at a higher level.

Note: In processes where this objective is in scope, it is fully covered through 6-6.4.1, 6-6.4.7b, and 6-6.4.7c.

Part 6 - Section 6.1 b:

b) to define the safety-related functionalities and properties of the software required for the implementation;

Process steps that apply: N/A

Justification:

Out of scope: In context, what is “required for the implementation” is to avoid violating a TSR allocated to software.

Note: In processes where this objective is in scope, it is fully covered through 6-6.4.1.

Part 6 - Section 6.1 c:

c) to refine the requirements of the hardware-software interface initiated in ISO 26262-4:2018, Clause 6; and

Process steps that apply: N/A

Justification:

This objective is fully covered through 6-6.4.4.

Part 6 - Section 6.1 d:

d) to verify that the software safety requirements and the hardware-software interface requirements are suitable for software development and are consistent with the technical safety concept and the system architectural design specification.

Process steps that apply: N/A

Justification:

This objective is fully covered through 6-6.4.7a, 6-6.4.7b, and 6-6.4.7c.

However, the parts of this objective concerning the TSC and system architectural design (covered through 6-6.4.7b and 6-6.4.7c) are out of scope.

11.5.2. Section 6.2

Part 6 - Section 6.2:

The technical safety requirements are refined and allocated to hardware and software during the system architectural design phase given in ISO 26262-4:2018, Clause 6. The specification of the software safety requirements considers in particular constraints of the hardware and the impact of these constraints on the software. This sub-phase includes the specification of software safety requirements to support the subsequent design phases.

Process steps that apply: N/A

Justification:

To the extent this general material introduces new process expectations, it is fully covered through the specific requirements below in 6-6.4.

11.5.3. Section 6.4

Part 6 - Section 6.4.1:

The software safety requirements shall be derived considering the required safety-related functionalities and properties of the software, whose failures could lead to the violation of a technical safety requirement allocated to software.

NOTE 1: The software safety requirements are either derived directly from the technical safety requirements allocated to software or are requirements for software functions and properties that, if not fulfilled, could lead to a violation of the technical safety requirements allocated to software.

EXAMPLE 1: Safety-related functionality of the software can be:

• functions that enable the safe execution of a nominal function;

• functions that enable the system to achieve or maintain a safe state or degraded state;

• functions related to the detection, indication and mitigation of faults of safety-related hardware elements;

• self-test or monitoring functions related to the detection, indication and mitigation of failures in the operating system, basic software or the application software itself;

• functions related to on-board and off-board tests during production, operation, service and decommissioning;

• functions that allow modifications of the software during production and service; or

• functions related to performance or time-critical operations.

EXAMPLE 2: Safety-related properties include robustness against erroneous inputs, independence or freedom from interference between different functionalities, or fault tolerance capabilities of the software.

NOTE 2: Safety-oriented analyses (see 7.4.10 or 7.4.11) can be used to identify additional software safety requirements or provide evidence for their achievement.

Process steps that apply: N/A

Justification:

Out of scope: This is applicable only at the top level of software safety requirements. Below the top level, higher-level software safety requirements capture all safety-related functionalities and properties of the software, though these may be refined per 6-7.4.6.

Part 6 - Section 6.4.2 a:

Specification of the software safety requirements derived from the technical safety requirements, the technical safety concept and the system architectural design in accordance with ISO 26262-4:2018, 6.4.1 and 6.4.3 shall consider:

1. the specification and management of safety requirements in accordance with ISO 26262-8:2018, Clause 6;

Process steps that apply:

See section entitled “ISO 26262-8:2018, Clause 6: Specification and management of safety requirements”

Justification:

See section entitled “ISO 26262-8:2018, Clause 6: Specification and management of safety requirements”

Part 6 - Section 6.4.2 b:

2. the specified system and hardware configurations;

EXAMPLE 1: Configuration parameters can include gain control, band pass frequency and clock prescaler.

Process steps that apply: N/A

Justification:

Out of scope: This is applicable only at the top level of software safety requirements.

Part 6 - Section 6.4.2 c:

3. the hardware-software interface specification;

Process steps that apply: N/A

Justification:

Out of scope: This is applicable only at the top level of software safety requirements.

Part 6 - Section 6.4.2 d:

4. the relevant requirements of the hardware design specification

Process steps that apply: N/A

Justification:

Out of scope: This is applicable only at the top level of software safety requirements.

Part 6 - Section 6.4.2 e:

5. the timing constraints

EXAMPLE 2 Execution or reaction time derived from the required response time at the system level.

Process steps that apply: Capture_Requirements

Justification:

The process requires to capture timing constraints at step Capture Requirements.

Part 6 - Section 6.4.2 f:

6. the external interfaces

EXAMPLE 3 Communication and user interfaces.

Process steps that apply:

• Identify_External_Packages

• Identify_Dependencies

• Capture_Requirements

Justification:

External interfaces and dependencies are identified at steps Identify External Interface Packages and Identify Dependencies. Step Capture Requirements prescribes that requirements allocated to the unit must include every responsibility of this unit stated by any software interface specification that this unit is responsible for complying with, as determined by the software architectural design.

Part 6 - Section 6.4.2 g:

7. each operating mode and each transition between the operating modes of the vehicle, the system, or the hardware, having an impact on the software.

EXAMPLE 4: Operating modes include shut-off or sleep, initialization, normal operation, degraded and advanced modes for testing or flash programming.

Process steps that apply: N/A

Justification:

Out of scope: Software impact of operating modes and operating mode transitions are encapsulated in higher-level software safety requirements.

Part 6 - Section 6.4.3:

If ASIL decomposition is applied to the software safety requirements, ISO 26262-9:2018, Clause 5, shall be complied with.

Process steps that apply: N/A

Justification:

Out of scope: This process currently only allows ASIL decomposition to occur at a higher level.

Part 6 - Section 6.4.4:

The hardware-software interface specification initiated in ISO 26262-4:2018, Clause 6, shall be refined sufficiently to allow for the correct control and usage of the hardware by the software, and shall describe each safety-related dependency between hardware and software.

Process steps that apply: N/A

Justification:

HSI refinement is out of scope of the process.

Part 6 - Section 6.4.5:

If other functions in addition to those functions for which safety requirements are specified in 6.4.1 are carried out by the embedded software, a specification of these functions and their properties in accordance with the applied quality management system shall be available.

Process steps that apply: N/A

Justification:

Out of scope: The quality management approach assumed by this process is Automotive SPICE, which does not expect any sort of software requirements to be specified below top-level.

Part 6 - Section 6.4.6:

The refined hardware-software interface specification shall be verified jointly by the persons responsible for the system, hardware and software development.

Process steps that apply: N/A

Justification:

HSI refinement is out of scope of the process.

Part 6 - Section 6.4.7 a:

The software safety requirements and the refined requirements of the hardware-software interface specification shall be verified in accordance with ISO 26262-8:2018, Clauses 6 and 9, to provide evidence for their:

1. suitability for software development;

Process steps that apply: N/A

Justification:

Fully covered in sections entitled “ISO 26262-8:2018, Clause 6: Specification and management of safety requirements” and “ISO 26262-8:2018, Clause 9: Verification”

Part 6 - Section 6.4.7 b:

2. compliance and consistency with the technical safety requirements;

Process steps that apply: N/A

Justification:

Out of scope: Verification of SSRs against TSRs is only applicable to top-level SSRs.

Part 6 - Section 6.4.7 c:

3. compliance with the system design; and

Process steps that apply: N/A

Justification:

Out of scope: Verification of SSRs against the system design is only applicable to top-level SSRs.

Part 6 - Section 6.4.7 d:

4. consistency with the hardware-software interface.

Process steps that apply:

• Inspect_Unit_Design

• Verify_Project

Justification:

Consistency of formally-verified unit requirements with the HSI is verified at step Verify Project

Consistency of non-formally-verified unit requirements with the HSI refinement is verified at step Inspect Unit Design

11.5.4. Section 6.5

Part 6 - Section 6.5.1:

Software safety requirements specification resulting from requirements 6.4.1 to 6.4.3 and 6.4.5.

Process steps that apply: Capture_Requirements

Justification:

The set of requirements in the public part of external ADS files specified at step Capture Requirements is the subset of the unit safety requirements specification governed by this process.

Part 6 - Section 6.5.2:

Hardware-software interface (HSI) specification (refined) resulting from requirement 6.4.4.

NOTE: This work product refers to the same work product as given in ISO 26262-5:2018, 6.5.2.

Process steps that apply: N/A

Justification:

HSI refinement is out of the process scope. The process ensures consistency with HSI, but the process doesn’t define (refined) HSI as a work product.

Part 6 - Section 6.5.3:

Software verification report resulting from requirements 6.4.6 and 6.4.7.

Process steps that apply:

See section entitled “Software Unit Verification Checklist”

Justification:

Verification report exists in form of checklist, which is described in section entitled “Software Unit Verification Checklist”

11.6. ISO 26262-6:2018, Clause 8: Software unit design and implementation

11.6.1. Section 8.1

Part 6 - Section 8.1 a:

The objectives of this sub-phase are:

1. to develop a software unit design in accordance with the software architectural design, …

Process steps that apply:

• Declare_Types_States_And_Subprograms

• Capture_Requirements

• Verify_Formal_Requirement_Consistency

• Verify_Non_Formal_Requirement_Consistency

• Verify_Requirement_Correctness_And_Completeness

• Inspect_Unit_Design

• Verify_Project

Justification:

Every claim made in the SWAD about the unit is stated as

• Formally-stated requirement, i.e. a contract in the ADS file (Declare Types, States, and Subprograms, Capture Requirements), this is automatically verified (Verify Formal Requirement Consistency)

• Informal requirement (Capture Requirements), this is verified through manual inspection (Verify Non-Formal Requirement Consistency)

All the requirements are manually verified for correctness and completeness (Verify Requirement Correctness, Completeness and Adherence to Ada/SPARK Guidelines). The whole unit design is verified at Inspect Unit Design. The implementation is formally verified against the ADS file at step Verify Project.

Part 6 - Section 8.1 a:

…, the design criteria and …

Process steps that apply:

See 6-5.4.1 (a), 6-8.4.3 and 6-8.4.5 in the traceability tables

Justification:

Design criteria to choose design, modeling and implementation language (such as an unambiguous and comprehensible definition, modularity, abstraction, encapsulation, and the use of structured constructs) are addressed in 6-5.4.1 a).

Design criteria for comprehensibility, unambiguity, correctness, consistency and verifiability of the unit design are addressed in sections 6-8.4.3 and 6-8.4.5 of this table.

Part 6 - Section 8.1 a:

… and the allocated software requirements which supports the implementation and verification of the software unit; and

Process steps that apply:

• Declare_Types_States_And_Subprograms

• Capture_Requirements

• Verify_Formal_Requirement_Consistency

• Verify_Non_Formal_Requirement_Consistency

• Verify_Requirement_Correctness_And_Completeness

• Inspect_Unit_Design

• Verify_Project

Justification:

Allocated software requirements are either:

• Formally-stated requirement, i.e. a contract in the ADS file (Declare Types, States, and Subprograms, Capture Requirements), this is automatically verified (Verify Formal Requirement Consistency) and manually verified (Verify Requirement Correctness, Completeness and Adherence to Ada/SPARK Guidelines), and then the implementation is formally verified against the ADS file (Verify Project)

• Informal requirement (Capture Requirements), this is verified through manual inspection (Verify Non-Formal Requirement Consistency).

All the requirements are manually verified for correctness and completeness (Verify Requirement Correctness, Completeness and Adherence to Ada/SPARK Guidelines). The whole unit design is verified at Inspect Unit Design to ensure that the design fully implements the allocated requirements. The implementation is formally verified against the ADS file at step Verify Project.

Part 6 - Section 8.1 b:

2. to implement the software units as specified.

Process steps that apply: Verify_Project

See sections entitled “Unit Implementation” and “Dynamic Verification”.

Justification:

Unit implementation in ADB file is created according to the section entitled “Unit Implementation”. The implementation is formally verified against formally-specified claims in the corresponding ADS file at step Verify Project. Non-formally-verified requirements are verified at steps Inspect Implementation and tested as described in section “Dynamic Verification”

11.6.2. Section 8.2

Part 6 - Section 8.2 paragraph 1:

Based on the software architectural design, the detailed design of the software units is developed. The detailed design can be represented in the form of a model.

Process steps that apply: N/A

Same as: Part 6 - Section 8.1 a

Part 6 - Section 8.2 paragraph 2:

The implementation at the source code level can be manually or automatically generated from the design in accordance with the software development environment.

Process steps that apply:

• Create_ADB

• Define_SPARK_Package

• Implement_SPARK_Package

Justification:

The implementation is created manually (no automatic generation involved) and resides in the ADB file.

The design is the combination of the ADS file and the ADB file (some aspects of the design may be captured in the ADS file).

Part 6 - Section 8.2 paragraph 3:

In order to develop a single software unit design, both software safety requirements and non-safety-related requirements are implemented. Hence, in this sub-phase, safety-related and non-safety-related requirements are handled within one development process.

Process steps that apply: N/A

Same as: Part 6 - Section 8.1 a

11.6.3. Section 8.4

Part 6 - Section 8.4.1:

The requirements of this sub-clause shall be complied with if the software unit is a safety-related element.

NOTE: “Safety-related” means that the unit implements safety requirements, or that the criteria for coexistence (see ISO 26262-9:2018, Clause 6) of the unit with other units are not satisfied.

Process steps that apply: Identify_Activity_Scope

Justification:

The process is complied with for all units that elect to use this process, whether safety-related or not.

Part 6 - Section 8.4.2 a:

The software unit design and implementation shall:

1. be suitable to satisfy the software requirements allocated to the software unit with the required ASIL;

Process steps that apply:

• Capture_Requirements

• Capture_Unit_Design_Constraints

• Document_Design_Solutions

• Inspect_Unit_Design

• Verify_Project

• Inspect_Implementation

  See section entitled “Dynamic Verification”

Justification:

For requirements that are formally-verified, the invocation of GNATprove in the Verify Project step ensures that the design and implementation satisfy the requirements with the required ASIL.

For requirements that are non-formally-verified, the Capture Unit Design Constraints and Document Design Solutions For Non-Formally-Verified Unit Specification Fragments steps collectively ensure that each such requirement is either re-specified formally or is mapped to a design documentation fragment that explains how the unit design satisfies the requirement with the required ASIL. The process also mandates creating traceability between non-formally-verified requirements and unit design. Verification is then done in the Inspect Unit Design and Inspect Implementation steps and as described in the section entitled “Dynamic Verification”.

Part 6 - Section 8.4.2 b:

b) be consistent with the software architectural design specification; and

Process steps that apply:

• Capture_Requirements

• Document_Design_Solutions

• Inspect_Unit_Design

• Verify_Project

• Inspect_Implementation

  See section entitled “Dynamic Verification”

Justification:

The Document Design Solutions For Non-Formally-Verified Unit Specification Fragments step mandates that the unit design be correct, consistent, and complete with respect to all the non-formally-verified requirements, including those in the software architectural design specification, captured in Capture Requirements. This is verified in the Inspect Unit Design and Inspect Implementation steps and as described in the section entitled “Dynamic Verification”.

Part 6 - Section 8.4.2 c:

c) be consistent with the hardware-software interface specification, if applicable.

Process steps that apply:

• Document_Design_Solutions

• Inspect_Unit_Design

Justification:

Building on the previous bullet, the non-formally-verified requirements also include those in hardware-software interface specifications applicable to the software unit as determined by the software architectural design.

Part 6 - Section 8.4.3 a:

To avoid systematic faults and to ensure that the software unit design achieves the following properties, the software unit design shall be described using the notations listed in Table 5.

1. consistency;

Process steps that apply:

• Document_Design_Solutions

• Inspect_Unit_Design

• Verify_Unit_Design

• Verify_Project

Justification:

To the extent that requirements and unit design fragments are formally-verified, GNATprove (in the Verify Unit Design and Verify Project steps) verifies the consistency of the unit design and the consistency of the implementation.

The Document Design Solutions For Non-Formally-Verified Unit Specification Fragments and Inspect Unit Design steps collectively ensure consistency across all (formally-verified and non-formally-verified) requirements and unit design fragments.

Part 6 - Section 8.4.3 b:

2. comprehensibility;

Process steps that apply:

• Inspect_Unit_Design

• Inspect_Implementation

Justification:

The in-context-comprehensibility of the unit design and implementation is verified in the Inspect Unit Design and Inspect Implementation steps, respectively.

Part 6 - Section 8.4.3 c:

3. maintainability; and

Process steps that apply:

• Capture_Unit_Design_Constraints

• Document_Design_Solutions

• Inspect_Unit_Design

• Verify_Unit_Design

Justification:

Optionally, some or all unit design constraints are formalized with SPARK (Capture Unit Design Constraints), and as such, are as maintainable as code itself.

Other unit design fragments are expressed non-formally in comments located in the source files, which helps to maintainability.

Additional verification steps (Document Design Solutions For Non-Formally-Verified Unit Specification Fragments, Inspect Unit Design, Verify Unit Design) help to maintainability.

Part 6 - Section 8.4.3 d:

4. verifiability.

Process steps that apply:

• Inspect_Unit_Design

• Verify_Unit_Design

• Verify_Project

  See section entitled “Dynamic Verification”

Justification:

Formal requirements and unit design constraints are verified by SPARK in step Verify Unit Design and later, entire unit implementation is verified in Verify Project

When unit design fragments cannot be fully formally proven with SPARK, the Inspect Unit Design step provides a procedure to verify them. All non-formally-verified claims in unit design are also tested as described in section entitled “Dynamic Verification”

Part 6 - Section 8.4.3 Table 5, 1a:

	A	B	C	D
Natural language	++	++	++	++

Natural language can complement the use of notations for example where some topics are more readily expressed in natural language or provide an explanation and rationale for decisions captured in the notations.

EXAMPLE To avoid possible ambiguity of natural language when designing complex elements, a combination of an activity diagram with natural language can be used.

Process steps that apply: Document_Design_Solutions

Justification:

The process requires for each non-formally-verified unit requirement and unit design fragment, where the unit design constraints and unit implementation are not sufficient to satisfy the non-formally-verified unit requirement and unit design fragments, to document how the unit design satisfies the unit requirement or unit design fragment at Document Design Solutions For Non-Formally-Verified Unit Specification Fragments step.

Note: Formally-verified requirements do not have to follow the same process as the risk that a formally-verified design fails to comply with its formally-verified requirement is sufficiently low.

Part 6 - Section 8.4.3 Table 5, 1b:

	A	B	C	D
Informal notations	++	++	+	+

Process steps that apply: Document_Design_Solutions

Justification:

Where natural language is insufficient to document a solution for satisfying a requirement or constraint, the Document Design Solutions For Non-Formally-Verified Unit Specification Fragments step requires the use of notations, whether informal, semi-formal, or formal.

Part 6 - Section 8.4.3 Table 5, 1c:

	A	B	C	D
Semi-formal notations	+	+	++	++

Semi-formal notations can include pseudocode or modeling with UML(R), SysML(R), Simulink(R) or Stateflow(R).

NOTE UML(R), SysML(R), Simulink(R) and Stateflow(R) are examples of suitable products available commercially. This information is given for the convenience of users of this document and does not constitute an endorsement by ISO of these products.

Process steps that apply:

• Document_Design_Solutions

• Inspect_Unit_Design

Justification:

If the unit is developed to ASIL C or ASIL D, then any informal argumentation must be supported with semi-formal notation (e.g. UML) as specified in the Document Design Solutions For Non-Formally-Verified Unit Specification Fragments step and verified at step Inspect Unit Design.

Part 6 - Section 8.4.3 Table 5, 1d:

	A	B	C	D
Formal notations	+	+	+	+

Process steps that apply: Capture_Unit_Design_Constraints

Justification:

Optionally, some/all unit design constraints are formalized with SPARK contracts as mentioned in the Capture Unit Design Constraints step.

Note that ISO 26262 recommends, but does not highly recommend, the use of formal notations. Consequently, we have freedom in this process to determine where it is appropriate to apply formal notations, and to allow other notations to be used in other contexts.

Part 6 - Section 8.4.4:

The specification of the software units shall describe the functional behaviour and the internal design to the level of detail necessary for their implementation.

EXAMPLE: Internal design can include constraints on the use of registers and storage of data.

Process steps that apply:

• Capture_Unit_Design_Constraints

• Document_Design_Solutions

• Inspect_Unit_Design

• Verify_Unit_Design

Justification:

The outcome of the unit design steps in this process is a complete set of ADS files that precisely define the boundaries of each library item, with a combination of formal and non-formal unit requirements and unit design fragments.

The ADS files are then ready to implement with ADB files.

Part 6 - Section 8.4.5 a:

Design principles for software unit design and implementation at the source code level as listed in Table 6 shall be applied to achieve the following properties:

1. correct order of execution of subprograms and functions within the software units, based on the software architectural design;

Process steps that apply:

• Capture_Requirements

• Capture_Unit_Design_Constraints

• Verify_Project

• Inspect_Implementation

  See section entitled “Dynamic Verification”

Justification:

Formal specifications in SPARK are attached to design elements. In particular, preconditions and postconditions are attached to subprogram declarations. In steps Capture Requirements and Capture Unit Design Constraints, it is suggested to express constraints (including ordering constraints) and requirements formally using SPARK aspects, if possible. Correct order of execution is then formally verified at Verify Project step.

If an ordering constraint is not formally specified it must be specified informally (Capture Requirements, Capture Unit Design Constraints). And verified at step Inspect Implementation and as described in section entitled “Dynamic Verification”

Part 6 - Section 8.4.5 b:

2. consistency of the interfaces between the software units;

Process steps that apply:

• Capture_Requirements

• Declare_Types_States_And_Subprograms

• Implement_SPARK_Package

Justification:

The Capture Requirements step requires to correctly transcribe non-SPARK interfaces from the SWAD into SPARK interfaces. SPARK interfaces from the SWAD are used as-is so there is no risk of inconsistency of interfaces.

Part 6 - Section 8.4.5 c:

c) correctness of data flow and control flow between and within the software units;

Process steps that apply:

• Verify_Project

• Document_Design_Solutions

• Inspect_Unit_Design

Justification:

For formally-verified requirements, GNATprove in the Verify Project step formally verifies that the data flow and control flow within the unit and between the units is correct, complete, and consistent with respect to those formally-verified requirements. These formally-verified requirements include any SPARK contracts inside the public parts of external ADS files concerning subprograms implemented in SPARK, if the contracts constrain data flow or control flow via Global and/or Depends aspects or postconditions. GNATprove additionally verifies that variables are initialized before being read and that variables are potentially read after being written.

For non-formally-verified requirements, the Document Design Solutions For Non-Formally-Verified Unit Specification Fragments step requires the unit design to explain how it achieves the correct flow of data and control both within the software unit and between it and other software units. This is then inspected in the Inspect Unit Design step.

Part 6 - Section 8.4.5 d:

4. simplicity;

Process steps that apply:

• Automated_Check_Against_Coding_Std

• Fix_Coding_Std_Issues

• Review_Diagnostic_Justifications

Justification:

The Automated Check Against Coding Standard and Safety Manual, Fix Coding Standard and Safety Manual Violations, and Review Diagnostic Justifications steps help to keep the code simple through running GNATcheck checks that monitor the complexity of the code and prevent the use of overly complex code. This includes limiting the McCabe cyclomatic complexity of non-proven code; see 6-5.4.3 Table 1 1a). (In proven SPARK code, McCabe cyclomatic complexity is not enforced, because complexity-induced systematic faults in that case are already sufficiently mitigated by the prover.)

Part 6 - Section 8.4.5 e:

5. readability and comprehensibility;

Process steps that apply:

• Capture_Requirements

• Declare_Types_States_And_Subprograms

• Capture_Unit_Design_Constraints

• Inspect_Unit_Design

• Inspect_Implementation

• Automated_Check_Against_Coding_Std

• Fix_Coding_Std_Issues

Justification:

Specification files contain the design for a unit, while the corresponding implementation is left to corresponding implementation files. This helps ensure that the design can be expressed in a readable and comprehensible format, free from the details of implementation.

The design and implementation is reviewed to ensure that they are in-context-comprehensible and observe Ada/SPARK Guidelines.

Automated checks help identifying guidelines violations to further improve readability.

Part 6 - Section 8.4.5 f:

6. robustness;

EXAMPLE: Methods to prevent implausible values, execution errors, division by zero, and errors in the data flow and control flow.

Process steps that apply:

• Static_Analysis_Unit

• Verify_Project

• Implement_SPARK_Package

• Verify_Dynamic_Assumptions

  “Dynamic Verification” section

Justification:

For non-proven units, a combination of CodePeer verifications (Static Analysis (Unit) step) and test (Dynamic Verification section) identifies likely error locations in the code. This supports potential software error detection and analysis throughout the code.

If a subprogram calls other subprograms, all the return values must be consumed and all errors must be properly handled by the subprogram (for SPARK code, GNATprove is able to detect most of these cases, for non-SPARK code it is done through manual inspection).

CodePeer provides various verifications looking at potential values and boundaries values of variables such as detection of attempts to dereference a variable that could be null, values outside the bounds of an Ada type or subtype, buffer overflows, numeric overflows or wraparounds, and divisions by zero. It also helps confirm expected boundary values of variables and parameters coming from the design.

To complement static analysis findings, tests are developed specifically to look at boundary values. All tests are run with full Ada checks on, together with additional validity checks, to catch during testing phases additional value errors that would be otherwise silent (see Verify Dynamic Assumptions).

When unit is proven, SPARK (Verify Project step) provides an exhaustive verification of various properties looking at potential values and boundaries values of variables such as detection of attempts to dereference a variable that could be null, values outside the bounds of an Ada type or subtype, buffer overflows, numeric overflows or wraparounds, and divisions by zero. It also helps confirm expected boundary values of variables and parameters coming from the design.

Part 6 - Section 8.4.5 g:

7. suitability for software modification; and

Process steps that apply:

• Capture_Requirements

• Declare_Types_States_And_Subprograms

• Capture_Unit_Design_Constraints

• Implement_SPARK_Package

• Inspect_Unit_Design

• Inspect_Implementation

Justification:

Requirements, unit design constraints and unit implementation are part of the code, and as such, as maintainable as code itself. In particular, since the compiler ensures consistency between the specification and implementation files for a unit, some consistency properties between the design and its implementation are maintained at all times.

When requirements are formally defined in contracts, the specification is also hosted in the ADS file. The verifier then ensures consistency between the specification, the design and the implementation.

The unit design and implementation are inspected against the Ada/SPARK Guidelines to ensure they are suitable for incremental modification.

Part 6 - Section 8.4.5 h:

8. verifiability.

Process steps that apply:

• Inspect_Unit_Design

• Inspect_Implementation

• Verify_Project

  See section entitled “Dynamic Verification”

Justification:

The implemented software shall be verified with a combination of inspections, tests and formal proofs.

When requirements and unit design constraints are defined in contracts, they are fully verifiable by proof.

Part 6 - Section 8.4.5 Table 6, 1a:

	A	B	C	D
One entry and one exit point in subprograms and functions	++	++	++	++

Process steps that apply:

• Verify_Project

• Automated_Check_Against_Coding_Std

  See section entitled “Ada/SPARK Guidelines”

Justification:

In Ada, a subprogram only has one entry.

One exit point recommendation is tailored in a separate document as described in the section entitled “Ada/SPARK Guidelines”.

Part 6 - Section 8.4.5 Table 6, 1b:

	A	B	C	D
No dynamic objects or variables, or else online test during their creation	+	++	++	++

Process steps that apply:

• Capture_Requirements

• Automated_Check_Against_Coding_Std

Justification:

The Ada allocator doesn’t return invalid state - instead it will cause an explicit error, calling directly the last chance handler allowing for diagnostic or recovery.

If such failures are not acceptable, allocation shall be forbidden through the usage of the local restrictions No_Heap_Allocations and No_Secondary_Stack (see Forward_Progress user aspect).

Part 6 - Section 8.4.5 Table 6, 1c:

	A	B	C	D
Initialization of variables	++	++	++	++

Process steps that apply:

• Verify_Project

• Static_Analysis_Unit

• Verify_Dynamic_Assumptions

Justification:

For a silver/gold SPARK unit, the Verify Project step provides exhaustive verification that all data read has been previously written to.

With non-proven units, the Static Analysis (Unit) step mandates the use of Codepeer that detects references to uninitialized variables.

This detection is complemented by the usage of Initialize_Scalars (Verify Dynamic Assumptions) which will put invalid values on uninitialized variables and, together with all checks enabled, will allow detection of additional cases of uninitialized variables.

Part 6 - Section 8.4.5 Table 6, 1d:

	A	B	C	D
No multiple use of variable names	++	++	++	++

Process steps that apply:

See section entitled “Requirements Concerning Compiler Warning Switches”

Justification:

Mandatory GNAT compiler switch -gnatwh activates warnings on hiding declarations so that in a given scope, only one reference to a variable name is visible.

Part 6 - Section 8.4.5 Table 6, 1e:

	A	B	C	D
Avoid global variables or else justify their usage	+	+	++	++

Process steps that apply:

• Capture_Requirements

• Implement_SPARK_Package

• Inspect_Implementation

• Verify_Project

Justification:

For non-SPARK subprogram bodies, the process requires providing global variable usage justification (Implement SPARK Package). This is verified through manual inspection (Inspect Implementation).

For SPARK subprograms, GNATprove enforces specification and verification of subprograms’ side effects, including usage of global variables: mandatory Global aspect makes intended usage of global variables explicit and easy to review, whereas GNATprove formally verifies that the implementation complies with this specification (Verify Project step). It sufficiently reduces the risk associated with the usage of global variables.

Part 6 - Section 8.4.5 Table 6, 1f:

	A	B	C	D
Restricted use of pointers	+	++	++	++

Process steps that apply:

• Verify_Project

• Inspect_Implementation

  See section entitled “Ada/SPARK Guidelines”

Justification:

In SPARK use of pointers is restricted by prohibiting aliasing. This restriction enables GNATprove to formally prove (step Verify Project) that use of pointers cannot result in runtime errors.

For non-SPARK code, use of pointers is restricted (see section entitled “Ada/SPARK Guidelines”). This is verified through manual inspection (Inspect Implementation)

Part 6 - Section 8.4.5 Table 6, 1g:

	A	B	C	D
No implicit type conversions	+	++	++	++

Process steps that apply: Compile_Project

Justification:

Ada does not allow implicit type conversions.

Part 6 - Section 8.4.5 Table 6, 1h:

	A	B	C	D
No hidden data flow or control flow	+	++	++	++

Process steps that apply:

• Declare_Types_States_And_Subprograms

• Implement_SPARK_Package

• Automated_Check_Against_Coding_Std

Justification:

Most cases of hidden data flow are not possible in Ada as they are not part of the language definition. Notably, the absence of preprocessor and the fact that case statements have a systematic break at the end of each alternative.

Part 6 - Section 8.4.5 Table 6, 1i:

	A	B	C	D
No unconditional jumps	++	++	++	++

Process steps that apply: Automated_Check_Against_Coding_Std

Justification:

Mandatory GNATcheck rule Unconditional_GOTO_statements restricts the use of any GOTO statement that is not directly contained within an if/then/else or case/when statement.

An EXIT statement in loop context is allowed:

• It is cleaner and less error-prone solution in comparison with alternatives, when exit from nested loops is required

• Syntactic constraints make it harder to abuse

Part 6 - Section 8.4.5 Table 6, 1j:

	A	B	C	D
No recursions	+	+	++	++

Process steps that apply:

• Create_Project_File

• Automated_Check_Against_Coding_Std

• Inspect_Unit_Design

• Inspect_Implementation

• Automated_Check_Against_Coding_Std_Integration

  See section entitled “Ada/SPARK Guidelines”

  See section entitled “Requirements Concerning GNATcheck Switches and Rules”

Justification:

These rules are verified by combination of automated style checks with GNATcheck and manual inspections to ensure that the code complies with Ada/SPARK Guidelines (which, per the Ada/SPARK Guidelines section, must specify how the organization is to comply with this recommendation in ISO 26262).

11.6.4. Section 8.5

Part 6 - Section 8.5.1 :

Software unit design specification resulting from requirements 8.4.2 to 8.4.5.

NOTE: In the case of model-based development, the implementation model and supporting descriptive documentation, using methods listed in Tables 5 and 6, specifies the software units.

Process steps that apply:

• Identify_Internal_Packages

• Create_Internal_ADS

• Declare_Internal_Types_States_And_Subprograms

• Capture_Unit_Design_Constraints

• Document_Design_Solutions

• Inspect_Unit_Design

• Verify_Unit_Design

Justification:

The software unit design specification is the outcome of the unit design steps.

Part 6 - Section 8.5.2 :

Software unit implementation resulting from requirement 8.4.5.

Process steps that apply:

• Create_ADB

• Define_SPARK_Package

• Implement_SPARK_Package

• Compile_Project

Justification:

The software unit implementation is the outcome of the unit implementation.

11.7. ISO 26262-6:2018, Clause 9: Software unit verification

11.7.1. Section 9.1

Part 6 - Section 9.1 a:

The objectives of this sub-phase are:

1. to provide evidence that the software unit design satisfies the allocated software requirements and is suitable for the implementation;

Process steps that apply:

• Capture_Requirements

• Verify_Formal_Requirement_Consistency

• Verify_Non_Formal_Requirement_Consistency

• Verify_Requirement_Correctness_And_Completeness

• Identify_Internal_Packages

• Create_Internal_ADS

• Declare_Internal_Types_States_And_Subprograms

• Capture_Unit_Design_Constraints

• Inspect_Unit_Design

• Verify_Unit_Design

• Verify_Project

Justification:

Formally-proven requirements are verified against unit design that specifies types, interfaces and data. They are also verified against the implementation (Verify Project).

When software requirements are not specified or proved in SPARK, an inspection is done to verify the consistency of data specified during the unit design phase with software requirements.

Part 6 - Section 9.1 b:

b) to verify that the defined safety measures resulting from safety-oriented analyses in accordance with 7.4.10 and 7.4.11 are properly implemented;

Process steps that apply:

• Capture_Requirements

• See Part 6 - Section 9.1 a

• See Part 6 - Section 9.1 c

Justification:

According to the process, any safety measures resulting from safety-oriented analyses must be captured as unit requirements in ADS file (Capture Requirements). See 6-9.1 a & c for how the process ensures that these requirements are properly implemented

Part 6 - Section 9.1 c:

c) to provide evidence that the implemented software unit complies with the unit design and fulfils the allocated software requirements with the required ASIL; and

Process steps that apply:

• Verify_Project

• Inspect_Unit_Design

• Inspect_Implementation

  “Dynamic Verification” section

Justification:

Compliance with formally-specified requirements and formally-specified claims in unit design is formally-verified by GNATprove at step Verify Project.

Compliance with informal requirements and informal parts of the unit design is verified through the manual inspection (Inspect Unit Design, Inspect Implementation) and testing (Dynamic Verification section)

Part 6 - Section 9.1 d:

d) to provide sufficient evidence that the software unit contains neither undesired functionalities nor undesired properties regarding functional safety.

Process steps that apply:

• Capture_Requirements

• Unit_Test_Run_And_Coverage

• Handle_Coverage_Deviations

Justification:

In fully formally verified code, in order to reduce the possibility of unintended functionality, the following is done: effects are specified and verified automatically, so we know exactly which variables are read and written; contracts express fully the requirements over changes to data; proof ensures that these contracts are fully respected.

If the unit is not fully formally verified, manual inspection of the implementation is performed, coverage is run against functional tests and deviations are addressed.

11.7.2. Section 9.2

Part 6 - Section 9.2 paragraph 1:

The software unit design and the implemented software units are verified by using an appropriate combination of verification measures such as reviews, analyses and testing.

Process steps that apply:

“Unit Verification” section

Justification:

Whenever reasonably possible, formal methods are used to verify software implementation - together with targeted static analysis and reviews.

A combination of static analysis, unit testing and reviews is performed on non-formally verified software.

Part 6 - Section 9.2 paragraph 2:

In order to verify a single software unit design, both software safety requirements and all non-safety-related requirements are considered. Hence in this sub-phase safety-related and non-safety-related requirements are handled within one development process.

Process steps that apply: Capture_Requirements

Section entitled “Unit Verification”

Justification:

This process requires the unit design to consider both safety- and non-safety related requirements (Capture Requirements).

During the verification (Unit_Verification), the process does not differentiate safety- and non-safety requirements.

11.7.3. Section 9.4

Part 6 - Section 9.4.1 :

The requirements of this sub-clause shall be complied with if the software unit is a safety-related element.

NOTE 1: “Safety-related element” according to ISO 26262-1 means that the unit implements safety requirements, or that the criteria for coexistence (see ISO 26262-9:2018, Clause 6) of the unit with other units are not satisfied.

NOTE 2: The requirements of this clause address safety-related software units; other software standards (see ISO 26262-2:2018, 5.4.5.1) can apply for verification of other software units.

NOTE 3: For model-based software development, the corresponding parts of the implementation model also represent objects for the verification planning. Depending on the selected software development process the verification objects can be the code derived from this model, the model itself, or both.

Process steps that apply:

See sections 6-9.4.2, 6-9.4.3 and 6-9.4.4

Justification:

6-9.4 is applicable to the process, because the process is designed for safety-related units.

See subsequent sections 6-9.4.2, 6-9.4.3 and 6-9.4.4, how the process complies to 6-9.4

Part 6 - Section 9.4.2 a:

The software unit design and the implemented software unit shall be verified in accordance with ISO 26262-8:2018, Clause 9 by applying an appropriate combination of methods according to Table 7 to provide evidence for:

1. compliance with the requirements regarding the unit design and implementation in accordance with Clause 8;

   NOTE 1: Software safety requirements include both functions and properties of the software.

   NOTE 2: Performing verification at the model level can substitute for verification at the source code level provided that the code generation preserves the properties (e.g. sufficient confidence in the code generators used).

   EXAMPLE: Evidence for the effective implementation of the error detection and error handling mechanisms specified to achieve robustness of the software unit against erroneous inputs.

Process steps that apply:

• Inspect_Unit_Design

• Verify_Unit_Design

• Verify_Project

  See section entitled “Unit Verification”

Justification:

Compliance with formally-verified requirements is verified by GNATprove in the Verify Unit Design and Verify Project steps.

Compliance with non-formally-verified requirements is verified in the Inspect Unit Design step (for the unit design) and by applying procedures described in section entitled “Unit Verification”, including: implementation inspection, testing, static code and coverage analyses

Part 6 - Section 9.4.2 b:

b) the compliance of the source code with its design specification;

NOTE 3: In the case of model-based development, requirement b) still applies.

Process steps that apply: Verify_Project

See section entitled “Unit Verification”

Justification:

Compliance with formally-specified parts of the unit design is verified by GNATprove at step Verify Project.

Compliance with informal parts of the unit design is verified by applying procedures described in section entitled “Unit Verification”, including: implementation inspection, testing, static code and coverage analyses

Part 6 - Section 9.4.2 c:

c) compliance with the specification of the hardware-software interface (in accordance with 6.4.4), if applicable;

Process steps that apply:

• Capture_Requirements

• See Part 6 - Section 9.4.2 a

Justification:

According to Capture Requirements, the requirements also include those in hardware-software interface specifications applicable to the software unit as determined by the software architectural design. Therefore, compliance with HSI is ensured if the unit design complies to all its requirements (see 6-9.4.2 (a) above).

Part 6 - Section 9.4.2 d:

4. confidence in the absence of unintended functionality and properties;

Process steps that apply:

• Capture_Requirements

• Verify_Project

• Verify_Formal_Requirement_Consistency

• Verify_Unit_Design

• Inspect_Implementation

• Verify_Non_Formal_Requirement_Consistency

• Verify_Requirement_Correctness_And_Completeness

• Inspect_Unit_Design

• Review_Tests

• Unit_Test_Run_And_Coverage

Justification:

For formally-verified unit, as described in section entitled “Capture Formal Requirements” [TFV13] gives a method on how to be confident in the absence of unintended functionality and properties:

• Requirements completeness is checked as part of the Verify Formal Requirement Consistency step

• Unintended dataflow are detected through the Verify Unit Design step

• the Verify Project step assures that the verification evidence is complete

• The manual inspection performed during the Inspect Implementation step to increase confidence that there is no unintended functionality.

When units are not fully proven, inspections are performed at different stages of the process in order to verify the completeness of the requirements, the unit design fragments, and the implementation, and to verify the consistency between requirements and unit design, between unit design and implementation. Finally, test coverage is performed at the unit level that checks code is fully covered.

Part 6 - Section 9.4.2 e:

e) sufficient resources to support their functionality and properties; and

Process steps that apply: Capture_Requirements

Section entitled “Unit Verification”

Justification:

According to the section entitled “Capture Requirements” necessary resource constraints must be specified as unit requirements. Therefore to ensure sufficiency of the resources it is enough to verify the completeness and consistency of the requirements and that the unit design and implementation comply with the requirements (Unit_Verification).

Part 6 - Section 9.4.2 f:

f) implementation of the safety measures resulting from the safety-oriented analyses in accordance with 7.4.10 and 7.4.11.

Process steps that apply: N/A

Justification:

The safety measures allocated to the software unit to implement are considered software unit requirements in this process and are handled accordingly.

Part 6 - Section 9.4.2 Table 7, 1a:

	A	B	C	D
Walk-through	++	+	o	o

For model-based development this method is applied at the model level, if evidence is available that justifies confidence in the code generator used.

Process steps that apply:

• Verify_Non_Formal_Requirement_Consistency

• Verify_Requirement_Correctness_And_Completeness

• Inspect_Unit_Design

• Review_Diagnostic_Justifications

• Review_Deactivated_SPARK

• Inspect_Implementation

  See section entitled “Assumptions About Change Management”

Justification:

Specific walkthroughs and reviews are implemented in the process to comply with this objective:

• Any change is reviewed by at least two persons (see section entitled “Assumptions about Change Management”)

• Non formally-specified requirements are verified at step Verify Non-Formal Requirement Consistency

• Requirements correctness and completeness is checked by manual review at step Verify Requirement Correctness, Completeness and Adherence to Ada/SPARK Guidelines

• Targeted reviews to justify GNATprove diagnostics and code with deactivated SPARK at steps Review Diagnostic Justifications, Review Deactivated SPARK

• Unit design and unit implementation inspections (Inspect Unit Design, Inspect Implementation)

Part 6 - Section 9.4.2 Table 7, 1b:

	A	B	C	D
Pair-programming	+	+	+	+

For model-based development this method is applied at the model level, if evidence is available that justifies confidence in the code generator used.

Process steps that apply: N/A

Justification:

While pair-programming is recommended by ISO 26262, this process does not require or recommend pair-programming.

Pair-programming is typically not feasible or effective due to the geographic diversity of engineers, the growing emphasis on working from home, and the varying speeds at which different engineers develop software or even type and read.

Part 6 - Section 9.4.2 Table 7, 1c:

	A	B	C	D
Inspection	+	++	++	++

For model-based development this method is applied at the model level, if evidence is available that justifies confidence in the code generator used.

Process steps that apply:

• Verify_Non_Formal_Requirement_Consistency

• Verify_Requirement_Correctness_And_Completeness

• Review_Deactivated_SPARK

• Inspect_Unit_Design

• Inspect_Implementation

Justification:

For units that cannot be proven, a manual inspection is done at each step of the development:

• Requirements that cannot be translated into contracts are consistent.

• Non SPARK subprograms are justified and the justification reviewed.

• Implementation is inspected to ensure it fulfills non-formal requirements.

For each proven unit, it is manually verified that requirements are fully described and correctly represented.

Implementation is inspected to check its compliance with Ada/SPARK design guidelines

Part 6 - Section 9.4.2 Table 7, 1d:

	A	B	C	D
Semi-formal verification	+	+	++	++

Process steps that apply:

• Verify_Dynamic_Assumptions

• Review_Deactivated_SPARK

Justification:

Where contracts are specified, the Verify Dynamic Assumptions step ensures that unless those contracts are disabled through pragma Assertion_Policy with the Ignore parameter (in which case the Review Deactivated SPARK step requires the development of additional test cases), the correctness of these contracts is verified during testing.

Part 6 - Section 9.4.2 Table 7, 1e:

	A	B	C	D
Formal verification	o	o	+	+

Process steps that apply: Verify_Project

Justification:

When contracts are expressed within the SPARK subset, the correctness of these contracts is formally verified.

Part 6 - Section 9.4.2 Table 7, 1f:

	A	B	C	D
Control flow analysis	+	+	++	++

This method can be applied at the source code level. This methods is applicable to both to manual code development and to model-based development.

This method can be part of methods 1e, 1h or 1i.

Process steps that apply:

• Document_Design_Solutions

• Inspect_Unit_Design

• Static_Analysis_Unit

• Static_Analysis_Integration

• Verify_Project

• Verify_Dynamic_Assumptions

• Unit_Test_Run_And_Coverage

Justification:

If the cleanliness-adjusted ASIL of the unit is ASIL C or ASIL D:

• Control and data flows must be documented with diagrams (Document Design Solutions For Non-Formally-Verified Unit Specification Fragments) and corresponding analyses are performed through manual inspection (Inspect Unit Design)

• CodePeer is used to 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; CodePeer also detects suspicious and potentially incorrect data flow. (Static Analysis (Unit), Static Analysis (Integration)).

This analysis is completed by structural code coverage analysis that detects code not exercised by tests (Unit Test Run And Coverage), which are run with Initialize_Scalars and additional checks to detect in run-time cases of uninitialized variables.

If the unit ASIL is ASIL C or ASIL D, but the cleanliness-adjusted ASIL of the unit is QM, ASIL A or ASIL B, there is no need to control and data flow analyses, because the risk that a formally-verified unit design and unit implementation (Verify Project) will fail to comply with its formally-specified ASIL C or ASIL D unit requirements and unit design constraints is sufficiently small (see argumentation in Inspect Unit Design).

Part 6 - Section 9.4.2 Table 7, 1g:

	A	B	C	D
Data flow analysis	+	+	++	++

This method can be applied at the source code level. This methods is applicable to both to manual code development and to model-based development.

This method can be part of methods 1e, 1h or 1i.

Process steps that apply: N/A

Same as: Part 6 - Section 9.4.2 Table 7, 1f

Part 6 - Section 9.4.2 Table 7, 1h:

	A	B	C	D
Static code analysis	++	++	++	++

Static analyses are a collective term which includes analysis such as searching the source code text or the model for patterns matching known faults or compliance with modelling or coding guidelines.

Process steps that apply:

• Static_Analysis_Unit

• Static_Analysis_Integration

• Verify_Project

• Automated_Check_Against_Coding_Std

• Automated_Check_Against_Coding_Std_Integration

Justification:

For non-SPARK Ada code, CodePeer is used in the Static Analysis (Unit) and Static Analysis (Integration) steps to identify potential errors via static analysis.

For SPARK code, GNATprove is used in the Verify Project step to prove compliance with formally-specified unit requirements and to prove the absence of run-time errors.

For all Ada code, GNATcheck is used in the Automated Check Against Coding Standard and Safety Manual and GNATcheck and gnatkp on whole program steps to enforce coding guidelines.

Part 6 - Section 9.4.2 Table 7, 1i:

	A	B	C	D
Static analyses based on abstract interpretation	+	+	+	+

Static analyses based on abstract interpretation are a collective term for extended static analysis which includes analysis such as extending the compiler parse tree by adding semantic information which can be checked against violation of defined rules (e.g. data-type problems, uninitialized variables), control-flow graph generation and data-flow analysis (e.g. to capture faults related to race conditions and deadlocks, pointer misuses) or even meta compilation and abstract code or model interpretation.

Process steps that apply: N/A

Same as: Part 6 - Section 9.4.2 Table 7, 1h

Part 6 - Section 9.4.2 Table 7, 1j:

	A	B	C	D
Requirements-based test	++	++	++	++

The software requirements at the unit level are the basis for this requirements-based test. These include the software unit design specification and the software safety requirements allocated to the software unit.

Process steps that apply: Verify_Project

See section entitled “Dynamic Verification”

Justification:

According to the process formally-specified and formally-verified with GNATprove requirements are not tested, because formal proofs provide enough confidence in the unit design and implementation.

Informal requirements are verified through testing. These test cases are derived from requirements and run with additional dynamic checking activated as described in the section entitled “Dynamic Verification”.

Part 6 - Section 9.4.2 Table 7, 1k:

	A	B	C	D
Interface test	++	++	++	++

This method can be used to provide evidence for the integrity of used and exchanged data.

Process steps that apply:

• Capture_Requirements

• Verify_Project

• Run_Integration_Tests

  Section entitled “Dynamic Verification”

Justification:

The process expects (Capture Requirements) that all interface constraints are captured as requirements (formal or not).

Interface constraints that are formally-proven, do not need to be tested, because the risk that the unit design and implementation do not meet corresponding requirements is low (Verify Project). Therefore a fully formally-proven unit doesn’t need interface tests at all.

Non formally-proven interface constraints must be tested as described in section entitled “Dynamic Verification”

The process also prescribes to run integration tests in two modes: normal and with full assertions on to enable additional dynamic checks to ensure that these errors are identified.

Part 6 - Section 9.4.2 Table 7, 1l:

	A	B	C	D
Fault injection test	+	+	+	++

In the context of software unit testing, fault injection test means to modify the tested software unit (e.g. introduce faults into the software) for the purposes described in 9.4.2. Such modifications include injection of arbitrary faults (e.g. by corrupting values of variables, by introducing code mutations, or by corrupting values of CPU registers).

Process steps that apply: Handle_Coverage_Deviations

Justification:

The Handle Coverage Deviations step forbids the use of “explained coverage” at ASIL D except when the explanation consists of formal verification. Where formal verification and dynamic testing do not together provide sufficient coverage of an ASIL D software unit, the Handle Coverage Deviations step expects fault injection tests to be used.

Part 6 - Section 9.4.2 Table 7, 1m:

	A	B	C	D
Resource usage evaluation	+	+	+	++

Some aspects of the resource usage evaluation can only be performed properly when the software unit tests are executed on the target environment or if the emulator for the target processor adequately supports resource usage tests.

Process steps that apply:

• Check_Stack_Usage_Unit

• Check_Stack_Usage_Integration

• Capture_Requirements

• Verify_Project

• Inspect_Implementation

  See section entitled “Dynamic Verification”

Justification:

To the extent resource usage constraints are expressed as requirements at Capture Requirements step, fulfillment of these constraints is verified by GNATprove for formally-specified requirements (Verify Project) or through inspection and testing for informal requirements (Inspect Implementation, section entitled “Dynamic Verification”)

Stack usage is checked in steps Check Stack Usage (Unit) and Check Stack Usage (Integration)

Part 6 - Section 9.4.2 Table 7, 1n:

	A	B	C	D
Back-to-back comparison test between model and code, if applicable	+	+	++	++

This method requires a model that can simulate the functionality of the software units. Here, the model and code are stimulated in the same way and results compared with each other.

EXAMPLE: In the case of model-based design results of non-floating-point operations can be compared.

Process steps that apply: N/A

Justification:

No model is used here, so back-to-back comparison tests are not applicable.

Part 6 - Section 9.4.3 Table 8, 1a:

To enable the specification of appropriate test cases for the software unit testing in accordance with 9.4.2, test cases shall be derived using the methods as listed in Table 8.

	A	B	C	D
Analysis of requirements	++	++	++	++

Process steps that apply:

• Verify_Project

• Write_Tests

Justification:

According to the process formally-specified and formally-verified with GNATprove requirements are not tested, because formal proofs provide enough confidence in the unit design and implementation.

Non formally-proven requirements are analyzed in step Write Tests, where necessary test cases are derived and implemented.

Part 6 - Section 9.4.3 Table 8, 1b:

	A	B	C	D
Generation and analysis of equivalence classes	+	++	++	++

Equivalence classes can be identified based on the division of inputs and outputs, such that a representative test value can be selected for each class.

Process steps that apply:

• Write_Tests

• Verify_Project

Justification:

According to the process formally-specified and formally-verified with GNATprove requirements are not tested, because formal proofs provide enough confidence in the unit design and implementation

Equivalence classes are derived from the non-formally-verified unit requirements, and corresponding tests are developed in step Write Tests.

Part 6 - Section 9.4.3 Table 8, 1c:

	A	B	C	D
Analysis of boundary values	+	++	++	++

This method applies to interfaces, values approaching and crossing the boundaries and out of range values.

Process steps that apply:

• Write_Tests

• Verify_Project

Justification:

According to the process formally-specified and formally-verified with GNATprove requirements are not tested, because formal proofs provide enough confidence in the unit design and implementation.

For non-formally-verified unit requirements, boundary values are analyzed and corresponding tests are developed in step Write Tests.

Part 6 - Section 9.4.3 Table 8, 1d:

	A	B	C	D
Error guessing based on knowledge or experience	+	+	+	+

Error guessing tests can be based on data collected through a “lessons learned” process and expert judgment.

Process steps that apply: N/A

Justification:

The process does not require this test derivation method to be applied, because other mandatory test derivation methods provide enough confidence that non formally-verified requirements are sufficiently covered.

Part 6 - Section 9.4.4:

To evaluate the completeness of verification and to provide evidence that the objectives for unit testing are adequately achieved, the coverage of requirements at the software unit level shall be determined and the structural coverage shall be measured in accordance with the metrics as listed in Table 9. If the achieved structural coverage is considered insufficient, either additional test cases shall be specified or a rationale based on other methods shall be provided.

NOTE 1: No target value or a low target value for structural coverage without a rationale is considered insufficient.

EXAMPLE 1: Analysis of structural coverage can reveal shortcomings in requirements-based test cases, inadequacies in requirements, dead code, deactivated code or unintended functionality.

EXAMPLE 2: A rationale can be given for the level of coverage achieved based on accepted dead code (e.g. code for debugging) or code segments depending on different software configurations; or code not covered can be verified using complementary methods (e.g. inspections).

EXAMPLE 3: A rationale can be based on the state of the art.

NOTE 2: The structural coverage can be determined by the use of appropriate software tools.

NOTE 3: In the case of model-based development, the analysis of structural coverage can be performed at the model level using analogous structural coverage metrics for models.

EXAMPLE 4: The analysis of structural coverage performed at the model level can replace the source code coverage metrics if it is shown to be equivalent, with rationales based on evidence that the coverage is representative of the code level.

NOTE 4: If instrumented code is used to determine the degree of structural coverage, it can be necessary to provide evidence that the instrumentation has no effect on the test results. This can be done by repeating representative test cases with non-instrumented code.

Process steps that apply:

• Unit_Test_Run_And_Coverage

• Handle_Coverage_Deviations

Justification:

Test coverage is performed when running unit tests. The coverage method depends on the cleanliness-adjusted ASIL of the unit (not the ASIL to which the unit is developed as described in Unit Test Run And Coverage):

• ASIL A: statement coverage

• ASIL B/C: statement and decision coverage

• ASIL D: statement and MC/DC coverage

As described in Handle Coverage Deviations, some types of gaps in coverage are allowed, in particular

• the uncovered statement, decision, or condition is part of a fully formally-verified subprogram, i.e., all the unit requirements or unit design constraints applicable to the subprogram are formally specified and the subprogram has SPARK mode on. In this case, the objectives of structural coverage as defined in ISO 26262-6:2018, 9.4.4 have already been achieved for the particular subprogram and there is no need to analyze the structural coverage of the subprogram

• the uncovered statement, decision, or condition is strictly necessary for GNATprove to be able to prove compliance with a type constraint (a range constraint or a null exclusion), an expression-based contract (a type predicate, a precondition of a called subprogram, or a postcondition of the incompletely-covered executable body), or an assertion pragma (pragma Assert, pragma Loop_Invariant, or pragma Loop_Variant)

Part 6 - Section 9.4.4 Table 9, 1a:

	A	B	C	D
Statement coverage	++	++	+	+

Process steps that apply: Unit_Test_Run_And_Coverage

Justification:

At cleanliness-adjusted ASIL A, statement coverage is used.

Part 6 - Section 9.4.4 Table 9, 1b:

	A	B	C	D
Branch coverage	+	++	++	++

Process steps that apply: Unit_Test_Run_And_Coverage

Justification:

At cleanliness-adjusted ASIL B/C, statement and decision coverage is used.

Part 6 - Section 9.4.4 Table 9, 1c:

	A	B	C	D
MC/DC (Modified Condition/Decision Coverage)	+	+	+	++

Process steps that apply: Unit_Test_Run_And_Coverage

Justification:

At cleanliness-adjusted ASIL D, statement and MC/DC coverage is used.

Part 6 - Section 9.4.5:

The test environment for software unit testing shall be suitable for achieving the objectives of the unit testing considering the target environment. If the software unit testing is not carried out in the target environment, the differences in the source and object code, as well as the differences between the test environment and the target environment, shall be analysed in order to specify additional tests in the target environment during the subsequent test phases.

NOTE 1: Differences between the test environment and the target environment can arise in the source code or object code, for example, due to different bit widths of data words and address words of the processors.

NOTE 2: Depending on the scope of the tests, the appropriate test environment for the execution of the software unit is used (e.g. the target processor, a processor emulator or a development system).

NOTE 3: Software unit testing can be executed in different environments, for example:

• model-in-the-loop tests;

• software-in-the-loop tests;

• processor-in-the-loop tests; or

• hardware-in-the-loop tests.

NOTE 4: For model-based development, software unit testing can be carried out at the model level followed by back-to-back comparison tests between the model and the object code. The back-to-back comparison tests are used to ensure that the behaviour of the models with regard to the test objectives is equivalent to the automatically-generated code.

Process steps that apply:

Section entitled “Process Binding”

Justification:

Test environment and its suitability argument are documented in the supplementary “Ada/SPARK Process Binding” document.

11.7.4. Section 9.5

Part 6 - Section 9.5.1:

Software verification specification resulting from requirements 9.4.2 to 9.4.5.

Process steps that apply:

• Identify_Activity_Scope

• Inspect_Unit_Design

• Review_Deactivated_SPARK

• Write_Tests

Justification:

The Software Unit Verification Specification is a separate work product that is constrained, but not defined, by this process (Inspect Unit Design).

Software Unit Verification Specification work product is initiated in Identify Activity Scope and then augmented in Review Deactivated SPARK and Write Tests.

Part 6 - Section 9.5.2:

Software verification report (refined) resulting from requirement 9.4.2.

Process steps that apply: Develop_Verification_Report

Justification:

At the end of the unit verification steps, a report is written that contains the outcome of all unit verification steps.

11.8. ISO 26262-8:2018, Clause 6: Specification and management of safety requirements

11.8.1. Section 6.1

Part 8 - Section 6.1 a:

The objectives of this clause are:

1. to ensure the correct specification of safety requirements with respect to their attributes and characteristics; and

Process steps that apply:

• Capture_Requirements

• Verify_Formal_Requirement_Consistency

• Verify_Non_Formal_Requirement_Consistency

• Verify_Requirement_Correctness_And_Completeness

Justification:

The process requires to split unit requirements into non-formal and formal ones. These requirements have to be specified in public part of external ADS file at step Capture Requirements

Formal requirements consistency is ensured at step Verify Formal Requirement Consistency (both internal and across all formal requirements). This step is performed automatically.

Non-formal requirements consistency of individual requirements and across all requirements is ensured at step Verify Non-Formal Requirement Consistency. This is done by manual review with an independent reviewer.

Part 8 - Section 6.1 b:

b) to ensure consistent management of safety requirements throughout the entire safety lifecycle.

Process steps that apply:

• Capture_Requirements

• Assign_Requirement_Unique_IDs

Justification:

The process requires assignment of unique ids to the requirements and establish traceability.

11.8.2. Section 6.2

Part 8 - Section 6.2 paragraph 1:

Safety requirements are requirements aimed at achieving and ensuring the required level of functional safety.

Process steps that apply: N/A

Justification:

This statement is considered in the below analysis of the rest of ISO 26262-8:2018, Part 6.

Part 8 - Section 6.2 paragraph 2:

During the safety lifecycle, safety requirements are specified and detailed in a hierarchical structure. The structure and dependencies of safety requirements used in the ISO 26262 series of standards are illustrated in Figure 2. The safety requirements are allocated or distributed among the elements.

Process steps that apply: N/A

Justification:

The process only concerns with development of software safety requirements (6-6). And only those of them which are allocated to software units

Part 8 - Section 6.2 paragraph 3:

The management of safety requirements includes obtaining agreement on them, obtaining commitments from those implementing the safety requirements, and maintaining traceability.

Process steps that apply:

• Capture_Requirements

• Document_Design_Solutions

Justification:

(The only applicable part is “maintaining traceability”.)

The process requires bidirectional trace links between the unit requirements and the corresponding claims in the software architectural design, responsibilities stated by interface specifications, and/or official requirements in software requirement management tools.

For non-formally-verified requirements, the process requires trace links to the documentation for how the unit design satisfies the requirement.

Part 8 - Section 6.2 paragraph 4:

In order to support the management of safety requirements, the use of suitable requirements management tools is recommended.

Process steps that apply:

See section entitled “Assumptions About Change Management”

Justification:

The process mandates to use configuration management tools to manage requirements status.

According to step Capture Requirements, the manner in which traceability information is recorded is outside the scope of this process.

Part 8 - Section 6.2 paragraph 5:

The specific requirements concerning the content of the safety requirements at different hierarchical levels are listed in ISO 26262-3, ISO 26262-4, ISO 26262-5 and ISO 26262-6.

Process steps that apply:

See section entitled “ISO 26262-6:2018, Clause 6: Specification of software safety requirements”

Justification:

See section entitled “ISO 26262-6:2018, Clause 6: Specification of software safety requirements”

11.8.3. Section 6.4

Part 8 - Section 6.4.1:

To achieve the characteristics of safety requirements listed in 6.4.2.4, safety requirements shall be specified by an appropriate combination of:

1. natural language; and

2. methods listed in Table 1.

An appropriate selection of methods for the specification of safety requirement considers their adequacy to achieve the characteristics of safety requirement according to 6.4.2 for a specific issue to be specified, its complexity or the knowledge of the persons specifying or managing safety requirements. Examples include the use of state graphs or diagrams for specifying the complex behaviour of software or hardware including many states or/and complex transitions.

Process steps that apply: Capture_Requirements

Justification:

According to the process, requirements are:

• Formally-specified in form of SPARK annotations

• Non-formal in form SPARK comments in ADS files

Non-formal requirements with ASIL C or D must be specified in semi-formal notation.

Part 8 - Section 6.4.1 Table 1, 1a:

	A	B	C	D
Informal notations for requirements specification	++	++	+	+

For higher level safety requirements (e.g. safety goals, functional and technical safety requirements) natural language and other types of informal notations are the most appropriate forms, though some requirements may be better handled with semi-formal notations.

Process steps that apply: Capture_Requirements

Justification:

Non-formal requirements can be specified with informal notation if their ASIL is ASIL B, ASIL A or QM.

Part 8 - Section 6.4.1 Table 1, 1b:

	A	B	C	D
Semi-formal notations for requirements specification	+	+	++	++

For higher level safety requirements (e.g. safety goals, functional and technical safety requirements) natural language and other types of informal notations are the most appropriate forms, though some requirements may be better handled with semi-formal notations.

Semi-formal notation formulates requirements using natural language that is supplemented by mathematical or graphical elements such as equations, graphs, diagrams, flow charts, timing diagrams, and many other forms of representation (e.g. UML (R) and SysML (TM)). Examples include model-based techniques and applying templates and controlled vocabulary for requirement sentences in natural language.

For lower-level safety requirements where precise hardware and software behaviours and capabilities may be specified, semi-formal notations are more appropriate due to greater clarity. However, even here it may not be possible or necessary to use semi-formal techniques for every requirement.

Process steps that apply: Capture_Requirements

Justification:

According to the process, non-formal safety requirements must be specified in semi-formal notation (EARS) if their ASIL is ASIL C or ASIL D.

It is recommended to use semi-formal notation for all requirements.

Part 8 - Section 6.4.1 Table 1, 1c:

	A	B	C	D
Formal notations for requirements specification	+	+	+	+

Process steps that apply: Capture_Requirements

Justification:

The process enables use of requirements, expressed in formal notation: SPARK contracts. Step Capture Requirements asks to transform as many software requirements as possible into appropriate SPARK annotations.

Formal notation is superior to informal and semi-formal, because it features fully specified syntax and semantics and enables rigorous automatic reasoning about them. So formal notation can be used in lieu of informal and semi-formal notations for any ASIL.

Part 8 - Section 6.4.2.1:

Safety requirements shall be unambiguously identifiable as safety requirements.

NOTE: In order to comply with this requirement, safety requirements can be listed in a separate document. If safety requirements and other requirements are administered in the same document, safety requirements can be identified explicitly by using a special attribute as described in 6.4.2.5.

Process steps that apply:

• Declare_Types_States_And_Subprograms

• Capture_Requirements

Justification:

The process requires each subprogram declared in an ADS file in a software interface specification to be explicitly assigned a specific ASIL or QM. If an ASIL is assigned, this is the ASIL of each requirement related to the subprogram, except for type predicates, type invariants, preconditions, and postconditions that are explicitly assigned lower ASILs.

This process requires each non-formal requirement to be explicitly assigned a specific ASIL or QM.

Part 8 - Section 6.4.2.2:

Safety requirements shall inherit the ASIL from the safety requirements from which they are derived, except if ASIL decomposition is applied in accordance with ISO 26262-9.

NOTE: As safety goals are the top level safety requirements, the inheritance of ASILs starts at the safety goal level.

Process steps that apply: N/A

Justification:

This process explicitly assumes that all requirements related to a software unit (including those specified in interfaces to other software units) have the same ASIL as the software unit itself. This assumption implies all ASILs are being inherited correctly.

Part 8 - Section 6.4.2.3:

Safety requirements shall be allocated to the item or element which implements them.

Process steps that apply: Capture_Requirements

Justification:

According to step Capture Requirements, software requirements allocated to the unit must include every claim about the unit in the SWAD, every responsibility imposed by interface specifications the unit must comply with, every official requirement allocated to the unit.

Note: unit requirements are allocated to the unit if they are specified in public part of external ADS file (Capture Requirements)

Part 8 - Section 6.4.2.4 a:

Safety requirements shall have the following characteristics:

NOTE 1: The characteristics for safety requirements enable clear communication to the stakeholders. They are the principle means of communicating the safety requirements to those who must implement them. The characteristics cited below are consistent with those referenced by ISO/IEC/IEEE 29148 (see Reference [8]).

1. unambiguous;

   NOTE 2: A requirement is unambiguous if there is a common understanding of the meaning of the requirement

Process steps that apply:

• Capture_Requirements

• Verify_Non_Formal_Requirement_Consistency

Justification:

SPARK contracts are expressed in SPARK language, which has precise syntax and semantics. That means that every unit requirement expressed in SPARK has the only interpretation and thus is unambiguous.

For non-formal requirements with ASIL C and ASIL D, the process requires semi-formal notation, which facilitates unambiguity of the requirements.

Unambiguity of the non-formal requirements are verified by the inspection using the verification checklist.

Part 8 - Section 6.4.2.4 b:

2. comprehensible;

NOTE 3: A requirement is comprehensible if the stakeholders and the consumers of that requirement understand its meaning.

Process steps that apply:

• Capture_Requirements

• Verify_Non_Formal_Requirement_Consistency

Justification:

Formal requirements are expressed using formal notation (SPARK annotations). Formal notation improves comprehensibility, because it has fully defined syntax and semantics.

For non-formal requirements with ASIL C or ASIL D, comprehensibility is facilitated by using semi-formal notation

Out-of-context-comprehensibility is verified at step Verify Requirement Correctness, Completeness and Adherence to Ada/SPARK Guidelines

Part 8 - Section 6.4.2.4 c:

3. atomic (singular);

NOTE 4: Safety requirements at one hierarchical level are atomic when they are formulated in such a way that they cannot be divided into at least two independent safety requirements at the considered level. The achievement of this characteristic could contradict the achievement of the other essential characteristics of safety requirements. In such a case, atomicity can be considered as having less importance.

Process steps that apply:

• Capture_Requirements

• Verify_Non_Formal_Requirement_Consistency

Justification:

For formally-verified requirements, atomicity is not strictly necessary, because the risk that a non-atomic requirement is not consistent with other requirements and the unit design is largely mitigated by GNATprove formal proofs.

For non-formal safety requirements the process requires them to be atomic if it does not contradict other objectives (Capture Requirements). This is verified by the inspection using the verification checklist (Verify Formal Requirement Consistency)

Part 8 - Section 6.4.2.4 d:

4. internally consistent;

NOTE 5: A requirement is internally consistent if it contains no contradictions within itself.

Process steps that apply:

• Verify_Formal_Requirement_Consistency

• Verify_Non_Formal_Requirement_Consistency

Justification:

Formal requirements internal consistency is verified automatically at step Verify Formal Requirement Consistency by GNATprove.

Internal consistency of non-formal requirements are verified by manual review with a local peer review at step Verify Non-Formal Requirement Consistency.

Part 8 - Section 6.4.2.4 e:

5. feasible and achievable;

NOTE 6: A requirement is feasible if it can be implemented within the constraints of the item development (resources, state-of-the-art, etc.).

NOTE 7: A requirement can be accomplished technically, [if] it does not require major technology advances, and fits within item constraints (e.g., cost schedule, technical, legal, regulatory, etc.) acceptably.

Process steps that apply: Inspect_Unit_Design

Justification:

Feasibility is verified during design inspection at step Inspect Unit Design.

Part 8 - Section 6.4.2.4 f:

6. verifiable;

NOTE 8: A requirement is verifiable if means, at the level where it is specified, are available to check that the requirement is fulfilled.

NOTE 9: Collected evidence pertaining to an item shows the corresponding requirement has been satisfied. Verifiability is enhanced when the requirement is measureable.

Process steps that apply:

• Implement_SPARK_Package

• Document_Design_Solutions

• Verify_Project

• Review_Deactivated_SPARK

• Inspect_Implementation

• Write_Tests

• Review_Tests

Justification:

According to the process following means are available to verify that the requirements are fulfilled:

• GNATprove to formally prove that formal requirements in form of SPARK contracts are indeed fulfilled by the SPARK implementation at steps Implement SPARK Package, Verify Project.

• Global peer review with deactivated SPARK mode to ensure that they do respect SPARK rules (e.g. pointer aliasing is absent, postconditions are honored) at step Review Deactivated SPARK.

• Traceability between a non-formal requirement and the documentation for how the unit design satisfies the requirement at step Document Design Solutions For Non-Formally-Verified Unit Specification Fragments.

• Inspection of the unit implementation according to an appropriate inspection checklist to ensure that it satisfies all the non-formally-verified unit requirements at step Inspect Implementation.

• Development and verification of unit tests, which provide evidence that every non-formally-verified unit requirement is satisfied. This is done at steps Write Tests and Review Tests.

Part 8 - Section 6.4.2.4 g:

7. necessary;

NOTE 10: The requirement defines an essential capability, characteristic, constraint, and/or quality factor. If it is removed or deleted, a deficiency will exist which is not fulfilled by other capabilities of the product or process.

NOTE 11: The requirement is currently applicable and has not been made obsolete by the passage of time. Requirements with planned expiration dates or applicability dates are clearly identified.

Process steps that apply: Verify_Requirement_Necessity

Justification:

Necessity of the specified requirements is verified at step Verify Requirement Necessity. This is done by manual review with a local peer review.

Part 8 - Section 6.4.2.4 h:

8. implementation free;

NOTE 12: The requirement, while addressing what is necessary and sufficient for the item, avoids placing unnecessary constraints on the architectural design. The objective is to be implementation independent. The requirement states what is required, not how the requirement should be met.

Process steps that apply:

• Capture_Requirements

• Verify_Non_Formal_Requirement_Consistency

Justification:

The formal requirements are specified in the public part of external ADS files in form of pre/post-conditions, return policy and dependency specification. These constraints are inherently implementation free: they do not specify how outcomes are obtained.

The non-formal requirements are required to be implementation free at step Capture Requirements.

Step Verify Non-Formal Requirement Consistency ensures that no unnecessary constraints were imposed. This is done by manual review with a local peer review.

Part 8 - Section 6.4.2.4 i:

1. complete; and

NOTE 13: The stated requirement is clear without further amplification because it is measureable and sufficiently describes the capability and characteristics required to meet the stakeholder’s need.

Process steps that apply:

• Verify_Requirement_Correctness_And_Completeness

• Inspect_Unit_Design

Justification:

Completeness of the specified requirements is verified at step Verify Requirement Correctness, Completeness and Adherence to Ada/SPARK Guidelines and Inspect Unit Design. This is done by manual review with a local peer review.

Part 8 - Section 6.4.2.4 j:

10. conforming.

NOTE 14: The stated requirement conforms to applicable government, automotive industry and product standards, specifications and interfaces for which compliance is required.

Process steps that apply:

• Verify_Requirement_Correctness_And_Completeness

• Inspect_Unit_Design

Justification:

This process is designed to fulfill the ISO 26262 and industry standards.

Compliance with Ada/SPARK Guidelines is checked at Verify Requirement Correctness, Completeness and Adherence to Ada/SPARK Guidelines and Inspect Unit Design by manual review with a local peer review.

Part 8 - Section 6.4.2.5 a:

Safety requirements shall have the following attributes:

1. a unique identification remaining unchanged throughout the safety lifecycle;

   EXAMPLE 1: A unique identification of a requirement can be achieved in a variety of ways, such as subscripting each instance of the word “shall”, e.g. “The system shall9782 check…”, or numbering consecutively each sentence containing the word “shall”, e.g. “9782 In the case of … the system shall check …”.

Process steps that apply: Assign_Requirement_Unique_IDs

Justification:

As part of the Assign Requirement Unique IDs step, for each requirement (whether safety or non-safety) that is either (a) non-formally-verified or (b) depended upon by some other non-formally-verified requirement, a unique ID is assigned to the requirement.

An exception is made for formally-verified requirements that are only depended upon by other formally-verified requirements. A unique ID is not needed for such a requirement, even if it is a safety requirement, because:

1. No explicit traceability is needed, because the sufficiency of the ASIL of the requirement and of any requirements it depends upon is formally verified.

2. Any corruption of the safety requirement that has any impact on compliance with higher-level safety requirements would result in formal verification detecting the anomaly.

Part 8 - Section 6.4.2.5 b:

2. a status; and

EXAMPLE 2: A status of a safety requirement can be “proposed”, “assumed”, “accepted”, “reviewed”, “delivered” or “verified”.

Process steps that apply: Assign_Requirement_Unique_IDs

Justification:

The status of each safety requirement is defined via change management as explained in the Assign Requirement Unique IDs step.

Part 8 - Section 6.4.2.5 c:

3. an ASIL.

Process steps that apply:

• Declare_Types_States_And_Subprograms

• Capture_Requirements

Justification:

This process explicitly assumes that all requirements related to a software unit (including those specified in interfaces to other software units) have the same ASIL as the software unit itself (or, for availability requirements, either ASIL B or the ASIL of the software unit, whichever is lower). Therefore an ASIL does not need to be explicitly specified for each requirement.

Note: Availability requirements are limited to ASIL B because ISO 26262 highly recommends defensive measures for complying with ASIL C and ASIL D requirements, which would entail expensive fault recovery from any corruption. Safety software typically uses redundancy to minimize the amount of software with ASIL C/D availability requirements.

Part 8 - Section 6.4.3.1 a:

The set of safety requirements for an item, an element, which are derived from one or more safety goals shall have the following properties:

1. hierarchical structure;

   NOTE 1: Hierarchical structure means that safety requirements are structured in several successive levels as presented in Figure 2. These levels are always aligned to comply with the corresponding design phases. It is possible that there could be several levels of hierarchy within any of the design phases of Figure 2.

Process steps that apply: Capture_Requirements

Justification:

The process requires bidirectional trace links between the unit requirements and the corresponding claims in the software architectural design, responsibilities stated by interface specifications, and/or official requirements in software requirement management tools. Transitively, all the safety requirements (formal or not) are linked to higher level safety requirements, forming the hierarchy.

Part 8 - Section 6.4.3.1 b:

b) organizational structure according to an appropriate grouping scheme;

NOTE 2: Organization of safety requirements means that safety requirements within each level are grouped together, usually corresponding to the architecture.

Process steps that apply: Capture_Requirements

Justification:

According to the process, all the unit requirements are specified within the public part of external ADS files, which relate to the unit. This way the requirements are grouped together. More fine grained grouping is achievable by grouping data type declarations, functions, procedures and associated SPARK annotations in subpackages if needed.

Part 8 - Section 6.4.3.1 c:

3. completeness;

NOTE 3: Completeness means that the safety requirements at one level fully implement all safety requirements of the previous level.

Process steps that apply: Verify_Requirement_Correctness_And_Completeness

Justification:

The process requires for each software unit, to verify (manually with a local peer review) that the public parts of the external ADS files collectively fully encapsulate every required property of the unit as specified in the unit requirements and SWAD.

Part 8 - Section 6.4.3.1 d:

4. external consistency;

NOTE 4: Unlike internal consistency, in which an individual safety requirement does not contradict itself, external consistency means that multiple safety requirements do not contradict each other.

Process steps that apply:

• Verify_Formal_Requirement_Consistency

• Verify_Non_Formal_Requirement_Consistency

• Inspect_Unit_Design

• Verify_Project

Justification:

External consistency of formal unit requirements within a single software interface is verified at step Verify Formal Requirement Consistency by GNATprove.

External consistency of all unit requirements within a single software interface is verified by manual review with a local peer review at step Verify Non-Formal Requirement Consistency (assuming that the formal requirements subset has been already proved to be consistent in the Verify Formal Requirement Consistency step as described above).

External consistency of non-formally-verified requirements from different sources is verified in the Inspect Unit Design step.

External consistency of formally-verified requirements from different software interfaces is verified in the Verify Project step.

Part 8 - Section 6.4.3.1 e:

e) no duplication of information within any level of the hierarchical structure; and

NOTE 5: No duplication of information means that the content of safety requirements is not repeated in any other safety requirement at one single level of the hierarchical structure and this is true at each hierarchical level.

Process steps that apply:

• Verify_Non_Formal_Requirement_Consistency

• Verify_Project

Justification:

The process does not require the absence of duplication of information across formally-verified requirements (Verify Project), because the risk of introducing inconsistencies is small.

Absence of duplication within the set of non-formal requirements and between formal and non-formal requirements is verified at step Verify Non-Formal Requirement Consistency and confirmed by the inspection verification checklist.

Part 8 - Section 6.4.3.1 f:

6. maintainability.

NOTE 6: Maintainability means that the set of requirements can be modified or extended, e.g. by the introduction of new versions of requirements or by adding/removing requirements to the set of requirements.

NOTE 7: Maintainability is facilitated when each requirement meets all of the points of 6.4.2.4, and the set of requirements meets 6.4.3.1.

Process steps that apply: Capture_Requirements

See section entitled “Assumptions about Change Management”

Justification:

All the unit requirements are specified in SPARK ADS files either in form of SPARK annotations (formal) or in form of comments (non-formal). Therefore the requirements can be modified, extended, added or removed by changing corresponding ADS files.

This must be done according to the existing change management process (see section entitled “Assumptions About Change Management”).

Part 8 - Section 6.4.3.2 a:

Safety requirements shall be traceable with a reference being made to:

1. each source of a safety requirement at the next upper hierarchical level;

Process steps that apply: Assign_Requirement_Unique_IDs

Justification:

The process requires establishing trace links between the unit requirements and the corresponding claims in the software architectural design, responsibilities stated by interface specifications, and/or official requirements in software requirement management tools.

Part 8 - Section 6.4.3.2 b:

b) each derived safety requirement at the next lower hierarchical level, or to its realisation in the design; and

Process steps that apply: Document_Design_Solutions

Justification:

For non-formally-verified requirements, the process requires trace links to the documentation for how the unit design satisfies the requirement. If this documentation depends on any requirements allocated to other software units, the process requires trace links from the documentation to those requirements.

This process does not mandate analogous unit design and unit implementation traceability for formally-verified requirements, because the risk that a formally-verified design and implementation will fail to comply with its formally-specified requirements is sufficiently small that there is minimal benefit in establishing such traceability.

Part 8 - Section 6.4.3.2 c:

3. the verification specification in accordance with 9.4.2.

NOTE 1: Various types of traceability records such as requirement management system, electronic materials, etc., can be used.

NOTE 2: Traceability supports:

• the achievement of consistency between a requirement, its realisation and verification,

• the effectiveness of an impact analysis if changes are made to particular safety requirements, and

• the execution of confirmation measures (e.g. functional safety assessment to evaluate the achieved functional safety).

Process steps that apply:

• Verify_Project

• Write_Tests

Justification:

For formally-verified requirements, there is no need to create tests and test specifications. Formal verification is performed at at steps Verify Formal Requirement Consistency and Verify Project.

For non-formally-verified requirements, the process requires to create trace links between each unit test and the unit requirements (Write Tests).

Part 8 - Section 6.4.3.3 :

An appropriate combination of the verification methods listed in Table 2 shall be applied to verify that the safety requirements comply with the requirements in this clause and that they comply with the specific requirements on the verification of safety requirements within the respective parts of the ISO 26262 series of standards where safety requirements are derived.

Process steps that apply:

• Verify_Non_Formal_Requirement_Consistency

• Verify_Requirement_Correctness_And_Completeness

• Inspect_Unit_Design

• Verify_Formal_Requirement_Consistency

• Verify_Project

Justification:

The process requires combination of two methods:

• Verification by inspection for all unit requirements according to verification checklist

• Formal verification for the formally specified unit requirement

Part 8 - Section 6.4.3.3 Table 2, 1a:

	A	B	C	D
Verification by walk-through	++	+	o	o

Process steps that apply: N/A

Justification:

N/A

Part 8 - Section 6.4.3.3 Table 2, 1b:

	A	B	C	D
Verification by inspection	+	++	++	++

Process steps that apply:

• Verify_Non_Formal_Requirement_Consistency

• Verify_Requirement_Correctness_And_Completeness

  See section entitled “Software unit verification checklist”

Justification:

Verification by inspection is applied to non-formal requirements at steps Verify Non-Formal Requirement Consistency.

Verification by inspection is applied to all captured requirements at step Verify Requirement Correctness, Completeness and Adherence to Ada/SPARK Guidelines and during the review according to the verification checklist.

Part 8 - Section 6.4.3.3 Table 2, 1c:

	A	B	C	D
Semi-formal verification	+	+	++	++

Verification can be supported by executable models.

Process steps that apply: N/A

Justification:

N/A

Part 8 - Section 6.4.3.3 Table 2, 1d:

	A	B	C	D
Formal verification	o	+	+	+

Verification can be supported by executable models.

Process steps that apply:

• Verify_Formal_Requirement_Consistency

• Verify_Unit_Design

• Verify_Project

Justification:

The formally-verified unit requirements are checked by GNATprove at the following process steps:

• Verify Formal Requirement Consistency: To verify the consistency of the formally-specified fragments of software interface specifications.

• Verify Unit Design: To verify the consistency of the formally-specified fragments of the unit design with one another and with the formally-specified requirements.

• Verify Project: To verify the consistency of all SPARK content in the ADS and ADB files and to verify all SPARK implementations fulfill all their contracts.

Part 8 - Section 6.4.3.4:

Safety requirements shall be placed under configuration management in accordance with Clause 7 to maintain consistency throughout the safety lifecycle.

EXAMPLE: When the safety requirements at a lower level are consistent with the higher level safety requirements, the configuration management can define a baseline as the basis for subsequent phases of the safety lifecycle.

Process steps that apply:

See section entitled “General Assumptions”

Justification:

Safety requirements are specified in SPARK ADS files, which are subject to configuration management.

11.9. ISO 26262-8:2018, Clause 9: Verification

Note: This clause is instantiated by:

• Part 6, Clause 6: Specification of software safety requirements

• Part 6, Clause 8: Software unit design and implementation

11.9.1. Section 9.1

Part 8 - Section 9.1:

The objective of verification is to ensure that the work products comply with their requirements.

Process steps that apply:

The sections entitled “Automated Static Verification”, Manual Static Verification, and “Static Verification”

Justification:

For formally-proven requirements and unit constraints, verification is done by means of formal proofs (the section entitled “Automated Static Verification”).

For non-formally-verified requirements a combination of manual inspections and testing is used (sections entitled Manual Static Verification and “Dynamic Verification”).

Verification is planned, specified and executed according to ISO 26262:2018 Part 8 9.4 (see below).

11.9.2. Section 9.2

Part 8 - Section 9.2:

Verification is applicable to the following phases of the safety lifecycle:

Process steps that apply:

The section entitled “Purpose of This Document”

Justification:

As stated in the section entitled “Purpose of This Document”, the process is only applicable to the product development phase.

Part 8 - Section 9.2 a:

Verification is applicable to the following phases of the safety lifecycle:

1. in the concept phase, verification ensures that the concept is correct, complete and consistent with respect to the boundary conditions of the item, and that the defined boundary conditions themselves are correct, complete and consistent, so that the concept can be realised;

Process steps that apply: N/A

Justification:

As stated in the section entitled “Purpose of This Document”, the process is only applicable to the product development phase.

Part 8 - Section 9.2 b:

b) in the product development phase, verification is conducted in different forms, as described below:

• In the design phases, verification is the evaluation of the work products, such as requirement specification, architectural design, models, or software code, thus ensuring that they comply with previously established requirements for correctness, completeness and consistency. Evaluation can be performed by review, simulation or analysis techniques. The evaluation is planned, specified, executed and documented in a systematic manner.

  NOTE: Design phases are ISO 26262-4:2018, Clause 6, ISO 26262-5:2018, Clause 7, ISO 26262-6:2018, Clause 7 and ISO 26262-6:2018, Clause 8.

• In the test phases, verification is the evaluation of the work products, items and elements within a test environment to ensure that they comply with their requirements. The tests are planned, specified, executed, evaluated and documented in a systematic manner.

Process steps that apply: N/A

Same as: Part 8 - Section 9.1

Part 8 - Section 9.2 c:

c) In the production and operation phase, verification ensures that:

• the safety-related special characteristics are appropriately met during production,

• the safety-related information is appropriately provided in the user manuals and in the repair and maintenance instructions; and

• the safety-related properties of the item are met by the application of control measures within the production process.

Process steps that apply: N/A

Justification:

As stated in the section entitled “Purpose of This Document”, the process is only applicable to the product development phase.

11.9.3. Section 9.4

Part 8 - Section 9.4.1.1:

The verification planning shall be carried out for each phase and sub-phase of the safety lifecycle and shall address the following:

Process steps that apply: Develop_Unit_Verification_Plan

Justification:

Each software unit is covered by a Software Unit Verification Plan.

Part 8 - Section 9.4.1.1 a:

1. the content of the work products to be verified;

Process steps that apply: Develop_Unit_Verification_Plan

Justification:

The Develop Unit Verification Plan step requires the Software Unit Verification Plan to identify the specific files and versions thereof containing the software unit design and implementation to be verified.

Part 8 - Section 9.4.1.1 b:

2. the objective of the verification;

Process steps that apply: Develop_Unit_Verification_Plan

Justification:

The Develop Unit Verification Plan step requires the Software Unit Verification Plan to state the objectives of software unit verification.

Part 8 - Section 9.4.1.1 c:

3. the methods used for verification;

Process steps that apply:

• Develop_Unit_Verification_Plan

• Inspect_Unit_Design

• Inspect_Implementation

• Verify_Project

• Static_Analysis_Unit

• Review_Tests

• Handle_Coverage_Deviations

• Verify_Dynamic_Assumptions

Justification:

The Develop Unit Verification Plan step requires the Software Unit Verification Plan to state that the methods of verification are defined in this document.

• The Inspect Unit Design and Inspect Implementation steps identify inspection as a verification method, and the conditions under which inspection is to be used.

• The Verify Dynamic Assumptions step specifies the runtime verification of contracts. This is a form of semi-formal verification.

• The Verify Project step specifies the use of GNATprove for formal verification of the SPARK code in the software unit.

• The Inspect Unit Design step specifies the use of control flow analysis and data flow analysis per the Ada/SPARK Process Binding.

• The Verify Project step specifies the use of GNATprove on SPARK code, with GNATprove configured in such a way as to verify the Absence of Runtime Errors. This verification requires static analysis, regardless of whether any additional contracts are present.

• The Static Analysis (Unit) step specifies the use of the CodePeer static analysis tool on non-SPARK code.

• The Verify Project and Review Tests steps in combination have the effect of requirements-based test and interface test.

• The Handle Coverage Deviations step specifies the use of fault injection testing under certain conditions.

Part 8 - Section 9.4.1.1 d:

4. the pass and fail criteria for the verification;

Process steps that apply: See Part 8 - Section 9.4.1.1 c

Justification:

The Develop Unit Verification Plan step requires the Software Unit Verification Plan to state that the verification pass/fail criteria are defined in this document.

Each process step related to software unit verification specifies the pass/fail criteria for the process step. In addition, this process compiles all these pass/fail criteria into a software unit verification checklist.

Part 8 - Section 9.4.1.1 e:

5. the verification environment, if applicable;

NOTE: A verification environment can be a test or simulation environment.

Process steps that apply: See Part 8 - Section 9.4.1.1 c

Justification:

The Develop Unit Verification Plan step requires the Software Unit Verification Plan to state that the verification environment is defined in this document.

The process steps related to software unit verification specify a combination of formal verification with theorem proving and dynamic testing.

Part 8 - Section 9.4.1.1 f:

6. the equipment used for verification, if applicable;

EXAMPLE: Test tools or measurement equipment.

Process steps that apply: See Part 8 - Section 9.4.1.1 c

Justification:

The Develop Unit Verification Plan step requires the Software Unit Verification Plan to state that some of the verification tools are defined in this document, and to identify any other tools or equipment needed for verification of the software unit.

The process steps related to software unit verification specify the particular GNAT tools that are expected to be used as part of verification.

Part 8 - Section 9.4.1.1 g:

7. the resources needed for verification, if applicable;

Process steps that apply: Develop_Unit_Verification_Plan

Justification:

The Develop Unit Verification Plan step requires the Software Unit Verification Plan to identify the resources needed to verify the software unit.

Part 8 - Section 9.4.1.1 h:

8. the actions to be taken if anomalies are detected; and

Process steps that apply: Develop_Unit_Verification_Plan

Justification:

The Develop Unit Verification Plan step requires the Software Unit Verification Plan to identify the actions to be taken if anomalies are detected during verification of the software unit.

Part 8 - Section 9.4.1.1 i:

1. the regression strategy.

NOTE: A regression strategy specifies how verification is repeated after changes have been made to the item or element. Verification can be repeated fully or partially and can include other items or elements that might affect the results of the verification.

Process steps that apply: Develop_Unit_Verification_Plan

Justification:

The Develop Unit Verification Plan step requires the Software Unit Verification Plan to identify the incremental software unit re-verification required after changes to the software unit design and/or implementation.

Part 8 - Section 9.4.1.2 a:

The planning of verification should consider the following:

1. the adequacy of the verification methods to be applied;

Process steps that apply: N/A

Justification:

The adequacy of the verification methods specified by this process is justified in this process itself (primarily in the traceability tables for ISO 26262-6:2018, Table 7) and in the collateral from the safety qualification of the GNAT tools.

Part 8 - Section 9.4.1.2 b:

2. the complexity of the work product to be verified;

Process steps that apply: N/A

Justification:

The complexity of software unit design and implementation is considered in this process itself in the determination of verification methods to apply.

Part 8 - Section 9.4.1.2 c:

c) prior experiences related to the verification of the subject material; and

NOTE: This includes service history as well as the degree to which a proven in use argument has been achieved.

Process steps that apply: N/A

Justification:

The verification approach defined in this process is informed by experience with the strengths and weaknesses of the various verification methods employed by this process.

Part 8 - Section 9.4.1.2 d:

d) the degree of maturity of the technologies used, or the risks associated with the use of these technologies.

Process steps that apply: N/A

Justification:

GNATprove is a mature verification tool, but nevertheless there are risks associated with the use of GNATprove in lieu of inspection and testing. These risks are analyzed as part of the safety qualification of GNATprove.

Part 8 - Section 9.4.2.1:

The verification specification shall specify the methods to be used for the verification, and shall include:

Process steps that apply:

• Identify_Activity_Scope

• Verify_Project

• Inspect_Unit_Design

• Write_Tests

  The section Manual Static Verification

Justification:

The process itself specifies the parts of the Verification Specification which relate to static verification. The Software Unit Verification Specification work product (as described in the Write Tests step) covers dynamic verification.

The Software Unit Verification Specification is a separate work product that is constrained, but not fully defined, by this process.

The Software Unit Verification Specification work product is initiated in the Identify Activity Scope step and then augmented during manual inspections and test development. See the Manual Static Verification section, the Inspect Unit Design step, and the Write Tests step.

The Software Unit Verification Specification is also expected to specify tests used to provide evidence for the validity of static check suppressions. See the Review Deactivated SPARK step.

Part 8 - Section 9.4.2.1 a:

1. review or analysis checklists, or

Process steps that apply: Inspect_Unit_Design

The section Manual Static Verification

Justification:

The process mandates unit design inspection and reviews/inspections of non-formally proven aspects of the implementation. All the inspections to be performed in accordance with inspection checklists.

Part 8 - Section 9.4.2.1 b:

2. simulation scenarios, or

Process steps that apply: N/A

Justification:

N/A

Part 8 - Section 9.4.2.1 c:

3. test cases, test data and test objects.

Process steps that apply: Write_Tests

Justification:

The process requires the existence of the Software Unit Specification Verification work product, which includes tests specifications as well as the rationale for their sufficiency.

Part 8 - Section 9.4.2.2:

For testing, the specification of each test case shall include the following:

1. a unique identification;

2. the reference to the version of the associated work product to be verified;

3. the preconditions and configurations;

   NOTE: If a complete verification of the possible configurations of a work product (e.g. variants of a system) is not feasible, a reasonable subset is selected (e.g. minimum or maximum functionality configurations of a system).

4. the environmental conditions, if appropriate;

   NOTE: Environmental conditions relate to the physical properties (e.g. temperature) of the surroundings in which the test is conducted or is simulated as part of the test.

5. the input data, their time sequence and their values;

6. the expected behaviour which includes output data, acceptable ranges of output values, time behaviour and tolerance behaviour; and

   NOTE 1: When specifying the expected behaviour, it can be necessary to specify the initial output data in order to detect changes.

   NOTE 2: It can be necessary to use an unambiguous reference to avoid the redundant specification and storage of preconditions, configurations and environmental conditions used for various test cases.

7. the criteria to determine the test case as passed or failed.

Process steps that apply: Write_Tests

Justification:

The process requires the existence of the Software Unit Specification Verification work product, where every test case is specified in accordance with ISO 262626-2018 Part 8, 9.4.2.2 and 9.4.2.3.

Part 8 - Section 9.4.2.3:

For testing, test cases shall be grouped according to the test methods to be applied, considering the following aspects:

1. the required test equipment or test environment;

2. the logical and temporal dependencies; and

3. the resources.

   EXAMPLE: Grouping of test cases for regression testing vs. full testing.

Process steps that apply: Write_Tests

Justification:

The process requires the existence of the Software Unit Specification Verification work product, where every test case is specified in accordance with ISO 262626-2018 Part 8, 9.4.2.2 and 9.4.2.3.

Part 8 - Section 9.4.2.4:

For testing, test cases should be reviewed by a different person regarding the author(s) of the work product to be verified.

Process steps that apply: Review_Tests

Justification:

According to the process the tests are reviewed with a local peer review.

Part 8 - Section 9.4.3.1:

The verification shall be executed as planned in accordance with 9.4.1 and specified in accordance with 9.4.2.

Process steps that apply:

• Develop_Unit_Verification_Plan

• Inspect_Unit_Design

• Unit_Test_Run_And_Coverage

• Verify_Dynamic_Assumptions

  The section Manual Static Verification

Justification:

As per the process, the verification is executed as planned (Develop Unit Verification Plan). In particular, static verification is executed as described in Inspect Unit Design and in the section Manual Static Verification. Dynamic verification is executed as described in Unit Test Run And Coverage and Verify Dynamic Assumptions, and in accordance with Software Unit Specification.

Part 8 - Section 9.4.3.2:

The verification should be performed by a different person regarding the author(s) of the work product to be verified.

Process steps that apply:

• Inspect_Unit_Design

• Review_Tests

  The section Manual Static Verification

Justification:

According to the process, all the inspections and reviews must be performed by a different person regarding the authors

Part 8 - Section 9.4.3.3:

The evaluation of the verification results shall contain the following information:

Process steps that apply:

• Automated_Check_Against_Coding_Std

• Verify_Project

• Unit_Test_Run_And_Coverage

• Static_Analysis_Unit

• Develop_Verification_Report

Justification:

The process requires that the dynamic verification results are evaluated in accordance with ISO 26262:2018 Part 8 9.4.3.3 and 9.4.3.4.

The results of static and dynamic verification are summarized in the Verification Report (Develop Verification Report).

Part 8 - Section 9.4.3.3 a:

1. the unique identification of the verified work product;

Process steps that apply:

• Develop_Unit_Verification_Plan

• Develop_Verification_Report

Justification:

The verification report must include reference to the Verification Plan (Develop Verification Report), which contains the unique identification of the verified work product (Develop Verification Report).

Part 8 - Section 9.4.3.3 b:

b) the reference to the verification plan and verification specification;

Process steps that apply: Develop_Verification_Report

Justification:

The verification report must reference the Software Unit Verification Specification and the Unit Verification Plan (Develop Verification Report).

Part 8 - Section 9.4.3.3 c:

c) the configuration of the verification environment and verification tools used and the calibration data used during the evaluation, if applicable;

Process steps that apply:

• Develop_Unit_Verification_Plan

• Unit_Test_Run_And_Coverage

• Develop_Verification_Report

Justification:

The process requires that the dynamic verification results are evaluated in accordance with ISO 26262:2018 Part 8 9.4.3.3.

The verification report must reference the Unit Verification Plan, which describes the verification environment, the verification tools defined in this document, including the particular version of this document that was used. It must identify any other tools or equipment used as part of verifying the software unit (Develop Verification Report).

Part 8 - Section 9.4.3.3 d:

d) the level of compliance of the verification results with the expected results;

Process steps that apply:

• Unit_Test_Run_And_Coverage

• Develop_Unit_Verification_Plan

Justification:

The process requires that the dynamic verification results are evaluated in accordance with ISO 26262:2018 Part 8 9.4.3.3.

Verification Plan identifies the actions to be taken if anomalies are detected during verification and the incremental re-verification required after changes to the software unit design and/or implementation.

Part 8 - Section 9.4.3.3 e:

e) an unambiguous statement of whether the verification passed or failed; if the verification failed the statement shall include the rationale for failure and suggestions for changes in the verified work product; and

NOTE: The verification is evaluated according to the criteria for completion and termination of the verification (see 9.4.1.1 d)) and to the expected verification results.

Process steps that apply:

• Unit_Test_Run_And_Coverage

• Develop_Verification_Report

Justification:

The process requires that the dynamic verification results are evaluated in accordance with ISO 26262:2018 Part 8 9.4.3.3.

The verification report contain an unambiguous statement of whether unit verification passed or failed (Develop Verification Report).

Part 8 - Section 9.4.3.3 f:

6. the reasons for any verification steps not executed.

Process steps that apply:

• Develop_Unit_Verification_Plan

• Unit_Test_Run_And_Coverage

• Develop_Verification_Report

Justification:

The process requires that the dynamic verification results are evaluated in accordance with ISO 26262:2018 Part 8 9.4.3.3.

The verification report must reference the Unit Verification Plan, which must identify the actions to be taken if anomalies are detected during verification.

Part 8 - Section 9.4.3.4:

The test equipment used for verification shall be able to deliver valid and reproducible results and shall be controlled in accordance with the applied quality management system.

Process steps that apply: Unit_Test_Run_And_Coverage

Justification:

The process requires that the dynamic verification results are evaluated in accordance with ISO 26262:2018 Part 8 9.4.3.4

11.9.4. Section 9.5

Part 8 - Section 9.5.1:

Verification plan resulting from requirements 9.4.1.1 and 9.4.1.2.

Process steps that apply: Develop_Verification_Report

Justification:

The process requires development of the verification plan to be completed at step Develop Verification Report.

Part 8 - Section 9.5.2:

Verification specification resulting from requirements 9.4.2.1 to 9.4.2.4.

Process steps that apply: Write_Tests

Justification:

The process requires development of Software Unit Verification Specification to be completed at step Write Tests.

Part 8 - Section 9.5.3:

Verification report resulting from requirements 9.4.3.1 to 9.4.3.4.

Process steps that apply: Develop_Verification_Report

Justification:

The process requires development of the Verification Report at step Develop Verification Report.