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

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

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.

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”.

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.

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.

Process steps that apply:

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.

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.

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.

Process steps that apply:

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

Process steps that apply:

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.

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.

Process steps that apply:

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.

Process steps that apply:

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).

Process steps that apply: N/A

Justification:

Strong typing is a native feature of the Ada language.

Process steps that apply:

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.

Process steps that apply:

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.

Process steps that apply: N/A

Justification:

Not covered.

Process steps that apply:

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.

Process steps that apply:

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.

Process steps that apply:

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

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

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.

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.

Process steps that apply: N/A

Justification:

This objective is fully covered through 6-6.4.4.

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

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

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.

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”

Process steps that apply: N/A

Justification:

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

Process steps that apply: N/A

Justification:

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

Process steps that apply: N/A

Justification:

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

Process steps that apply: Capture_Requirements

Justification:

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

Process steps that apply:

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.

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.

Process steps that apply: N/A

Justification:

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

Process steps that apply: N/A

Justification:

HSI refinement is out of scope of the process.

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.

Process steps that apply: N/A

Justification:

HSI refinement is out of scope of the process.

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”

Process steps that apply: N/A

Justification:

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

Process steps that apply: N/A

Justification:

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

Process steps that apply:

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

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.

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.

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

Process steps that apply:

Justification:

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

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.

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.

Process steps that apply:

Justification:

Allocated software requirements are either:

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.

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

Process steps that apply: N/A

Same as: Part 6 - Section 8.1 a

Process steps that apply:

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).

Process steps that apply: N/A

Same as: Part 6 - Section 8.1 a

11.6.3. Section 8.4

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.

Process steps that apply:

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”.

Process steps that apply:

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”.

Process steps that apply:

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.

Process steps that apply:

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.

Process steps that apply:

Justification:

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

Process steps that apply:

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.

Process steps that apply:

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”

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.

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.

Process steps that apply:

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.

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.

Process steps that apply:

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.

Process steps that apply:

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”

Process steps that apply:

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.

Process steps that apply:

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.

Process steps that apply:

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.)

Process steps that apply:

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.

Process steps that apply:

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.

Process steps that apply:

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.

Process steps that apply:

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.

Process steps that apply:

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”.

Process steps that apply:

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).

Process steps that apply:

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.

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.

Process steps that apply:

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.

Process steps that apply:

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)

Process steps that apply: Compile_Project

Justification:

Ada does not allow implicit type conversions.

Process steps that apply:

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.

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

Process steps that apply:

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

Process steps that apply:

Justification:

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

Process steps that apply:

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

Process steps that apply:

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.

Process steps that apply:

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

Process steps that apply:

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)

Process steps that apply:

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

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.

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

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

Process steps that apply:

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

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

Process steps that apply:

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).

Process steps that apply:

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:

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.

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).

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.

Process steps that apply:

Justification:

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

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.

Process steps that apply:

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

Process steps that apply:

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.

Process steps that apply: Verify_Project

Justification:

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

Process steps that apply:

Justification:

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

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).

Process steps that apply: N/A

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

Process steps that apply:

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.

Process steps that apply: N/A

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

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”.

Process steps that apply:

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.

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.

Process steps that apply:

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)

Process steps that apply: N/A

Justification:

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

Process steps that apply:

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.

Process steps that apply:

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.

Process steps that apply:

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.

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.

Process steps that apply:

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)

Process steps that apply: Unit_Test_Run_And_Coverage

Justification:

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

Process steps that apply: Unit_Test_Run_And_Coverage

Justification:

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

Process steps that apply: Unit_Test_Run_And_Coverage

Justification:

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

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

Process steps that apply:

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.

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

Process steps that apply:

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.

Process steps that apply:

Justification:

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

11.8.2. Section 6.2

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.

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

Process steps that apply:

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.

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.

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

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.

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.

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.

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.

Process steps that apply:

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.

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.

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)

Process steps that apply:

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.

Process steps that apply:

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

Process steps that apply:

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)

Process steps that apply:

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.

Process steps that apply: Inspect_Unit_Design

Justification:

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

Process steps that apply:

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.

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.

Process steps that apply:

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.

Process steps that apply:

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.

Process steps that apply:

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.

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.

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.

Process steps that apply:

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.

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.

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.

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.

Process steps that apply:

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.

Process steps that apply:

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.

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”).

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.

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.

Process steps that apply:

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).

Process steps that apply:

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

Process steps that apply: N/A

Justification:

N/A

Process steps that apply:

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.

Process steps that apply: N/A

Justification:

N/A

Process steps that apply:

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.

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

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

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.

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.

Process steps that apply: N/A

Same as: Part 8 - Section 9.1

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

Process steps that apply: Develop_Unit_Verification_Plan

Justification:

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

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.

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.

Process steps that apply:

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

Process steps that apply:

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.

Process steps that apply: Inspect_Unit_Design

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.

Process steps that apply: N/A

Justification:

N/A

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.

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.

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.

Process steps that apply: Review_Tests

Justification:

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

Process steps that apply:

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.

Process steps that apply:

Justification:

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

Process steps that apply:

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).

Process steps that apply:

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).

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).

Process steps that apply:

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).

Process steps that apply:

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.

Process steps that apply:

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).

Process steps that apply:

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.

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

Process steps that apply: Develop_Verification_Report

Justification:

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

Process steps that apply: Write_Tests

Justification:

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

Process steps that apply: Develop_Verification_Report

Justification:

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