Preamble

This is a collection of several related documents:

• The NVIDIA SPARK Process (GFDL v1.3) describing a software process using Ada/SPARK to meet ISO 26262.

• The Common document which contains the licenses and bibliography.

NVIDIA SPARK Process

Process:

• 1. License
• 2. Attribution
• 3. Introduction
  • 3.1. Disclaimer
  • 3.2. Foreword
  • 3.3. Purpose of This Document
  • 3.4. Outline of the Rest of This Document
  • 3.5. How To Read This Document
• 4. Terminology
  • 4.1. Software Unit (or Unit)
  • 4.2. Unit-Level Work Product
  • 4.3. Non-Unit-Level Work Product
  • 4.4. Software Unit Specification Fragment (or Unit Specification Fragment)
  • 4.5. Software Unit Requirement (or Unit Requirement)
  • 4.6. Software Unit Design Fragment (or Unit Design Fragment)
  • 4.7. Software Unit Design Constraint (or Unit Design Constraint)
  • 4.8. Design Documentation Fragment
  • 4.9. Diagnostic Justification
  • 4.10. Check Suppression
  • 4.11. Formal Unit Requirement or Formal Unit Design Constraint
  • 4.12. Non-Formal Unit Requirement or Non-Formal Unit Design Constraint
  • 4.13. Implementation Free Requirement
  • 4.14. Software Interface
  • 4.15. SPARK Platinum
  • 4.16. Clean SPARK
  • 4.17. Clean SPARK Platinum
  • 4.18. Cleanliness-Adjusted ASIL
  • 4.19. GPR File (or Project File)
  • 4.20. Unit GPR File (or Unit Project File)
  • 4.21. ADC File
  • 4.22. ADS File
  • 4.23. ADB File
  • 4.24. External ADS File
  • 4.25. Internal ADS File
  • 4.26. GNAT Project (or Project)
  • 4.27. Non-Formal Verification
  • 4.28. Formally-Verified
  • 4.29. Non-Formally-Verified
  • 4.30. Out-of-Context-Comprehensible
  • 4.31. In-Context-Comprehensible
  • 4.32. Local Peer Review
  • 4.33. Global Peer Review
• 5. Prerequisites and Assumptions
  • 5.1. General Assumptions
  • 5.2. Consistent ASIL
  • 5.3. Assumptions About the Technical Architecture
  • 5.4. Assumptions About Change Management
  • 5.5. Assumptions About Software Interface Specifications
  • 5.6. Ada/SPARK Process Binding
  • 5.7. Ada/SPARK Guidelines
  • 5.8. Integration Verification
• 6. Process
  • 6.1. Traceability Model
  • 6.2. Unit Requirements in ADS Files
  • 6.3. Unit Design
  • 6.4. Unit Implementation
  • 6.5. Unit Verification
  • 6.6. Integration Verification
• 7. Requirements Concerning Tool Switches
  • 7.1. Requirements Concerning Compiler Warning Switches
  • 7.2. Requirements Concerning Non-Warning-Related Compiler Switches
  • 7.3. Requirements Concerning GNATprove Switches
  • 7.4. Requirements Concerning GNATcheck Switches and Rules
• 8. Software Unit Verification Checklists
  • 8.1. Verification Checklist for Software Unit Requirements
  • 8.2. Verification Checklists for Software Unit Design and Implementation
• 9. Software Tool Usage Analysis
  • 9.1. GPRbuild
  • 9.2. GNATprove
  • 9.3. GNATstack
  • 9.4. GNATstub
  • 9.5. GNATcheck and GNATkp
  • 9.6. GNATcoverage
  • 9.7. CodePeer
• 10. Traceability to GNATprove Assumptions
  • 10.1. Shorthand used by the GNATprove Assumptions
  • 10.2. Terminology used by the GNATprove assumptions
  • 10.3. Generally Applicable Assumptions
  • 10.4. Assumptions For Mixing SPARK and Non-SPARK Code
  • 10.5. Assumptions For Modular Use of GNATprove
  • 10.6. Assumptions For Compiling SPARK With Non-GNAT Tools
• 11. Traceability to ISO 26262
  • 11.1. Attribution
  • 11.2. List of Objectives, Requirements, and Recommendations in ISO 26262 Fully Met By Following This Process
  • 11.3. Notation in the ISO 26262 Traceability Tables
  • 11.4. ISO 26262-6:2018, Clause 5: General topics for the product development at the software level
  • 11.5. ISO 26262-6:2018, Clause 6: Specification of software safety requirements
  • 11.6. ISO 26262-6:2018, Clause 8: Software unit design and implementation
  • 11.7. ISO 26262-6:2018, Clause 9: Software unit verification
  • 11.8. ISO 26262-8:2018, Clause 6: Specification and management of safety requirements
  • 11.9. ISO 26262-8:2018, Clause 9: Verification

Common

Common:

• 1. GNU Free Documentation License
  • 1.1. PREAMBLE
  • 1.2. APPLICABILITY AND DEFINITIONS
  • 1.3. VERBATIM COPYING
  • 1.4. COPYING IN QUANTITY
  • 1.5. MODIFICATIONS
  • 1.6. COMBINING DOCUMENTS
  • 1.7. COLLECTIONS OF DOCUMENTS
  • 1.8. AGGREGATION WITH INDEPENDENT WORKS
  • 1.9. TRANSLATION
  • 1.10. TERMINATION
  • 1.11. FUTURE REVISIONS OF THIS LICENSE
  • 1.12. RELICENSING
  • 1.13. ADDENDUM: How to use this License for your documents
• 2. Bibliography