6. Process

This section defines the steps of the SPARK-based process defined in this document.

It is expected that this process will be applied only to a subset of the software units (that subset will be identified in the Identify Activity Scope process step described below).

• 6.1. Traceability Model
  • 6.1.1. Assigning Traceability IDs to Content in ADS/ADB Files
• 6.2. Unit Requirements in ADS Files
  • 6.2.1. Identify External Interface Packages
    • 6.2.1.1. Nested packages allowed
    • 6.2.1.2. Note on packages hierarchies implemented by multiple distinct software units
    • 6.2.1.3. Situations where a package is spread among multiple object files
  • 6.2.2. Create External ADS
  • 6.2.3. Declare SPARK Package
  • 6.2.4. Identify Dependencies
  • 6.2.5. Declare Types, States, and Subprograms
  • 6.2.6. Capture Requirements
    • 6.2.6.1. Capture Formal Requirements
    • 6.2.6.2. Capture Non-Formal Requirements
    • 6.2.6.3. Public Expression Functions
  • 6.2.7. Assign Requirement Unique IDs
    • 6.2.7.1. Language bindings not considered requirements
    • 6.2.7.2. Rationale for not making exceptions for formal requirements
    • 6.2.7.3. Requirement status
  • 6.2.8. Verify Formal Requirement Consistency
  • 6.2.9. Verify Non-Formal Requirement Consistency
  • 6.2.10. Verify Requirement Correctness, Completeness and Adherence to Ada/SPARK Guidelines
  • 6.2.11. Verify Requirement Necessity
• 6.3. Unit Design
  • 6.3.1. Identify Activity Scope
  • 6.3.2. Create Project File
    • 6.3.2.1. Deferred Creation of the Project File
    • 6.3.2.2. Unneeded Packages in Auto-Generated Project Files
    • 6.3.2.3. Multiple Project Files For a Software Unit
    • 6.3.2.4. Multiple Software Units In a Project File
    • 6.3.2.5. Refactoring Project File Packages
  • 6.3.3. Create Configuration Pragmas
  • 6.3.4. Identify Internal Packages
    • 6.3.4.1. Non-Necessity of Internal Packages
    • 6.3.4.2. Regarding the Transcription of Interfaces
    • 6.3.4.3. Internal Package Naming Convention
  • 6.3.5. Create Internal ADS
  • 6.3.6. Declare Internal Types, States, and Subprograms
  • 6.3.7. Capture Unit Design Constraints
    • 6.3.7.1. Revisiting This Step
    • 6.3.7.2. Clean SPARK
  • 6.3.8. Document Design Solutions For Non-Formally-Verified Unit Specification Fragments
    • 6.3.8.1. ASIL vs. Cleanliness-Adjusted ASIL
    • 6.3.8.2. Traceability Not Required for Formally-Verified Unit Specification Fragments
    • 6.3.8.3. Revisiting This Step
  • 6.3.9. Inspect Unit Design
    • 6.3.9.1. Verification Work Products
    • 6.3.9.2. Implications and Timing of Unit Design Inspection
  • 6.3.10. Verify Unit Design
• 6.4. Unit Implementation
  • 6.4.1. Create ADB
  • 6.4.2. Define SPARK Package
  • 6.4.3. Implement SPARK Package
    • 6.4.3.1. Non-SPARK Ada
    • 6.4.3.2. Proof Suggestions
    • 6.4.3.3. Diagnostic Justifications
    • 6.4.3.4. Clean SPARK
    • 6.4.3.5. Non-Formally-Verified Unit Specification Fragments
  • 6.4.4. Compile Project
• 6.5. Unit Verification
  • 6.5.1. Develop Unit Verification Plan
  • 6.5.2. Automated Static Verification
    • 6.5.2.1. Verify Project
      • 6.5.2.1.1. Rationale For Invoking On Each Project
      • 6.5.2.1.2. Consistency
      • 6.5.2.1.3. Formal Verification of Generic Instantations
    • 6.5.2.2. Automated Check Against Coding Standard and Safety Manual
    • 6.5.2.3. Fix Coding Standard and Safety Manual Violations
    • 6.5.2.4. Static Analysis (Unit)
      • 6.5.2.4.1. Proven Code
      • 6.5.2.4.2. Multiple Project Files
    • 6.5.2.5. Check Stack Usage (Unit)
  • 6.5.3. Manual Static Verification
    • 6.5.3.1. Review Diagnostic Justifications
    • 6.5.3.2. Review Deactivated SPARK
      • 6.5.3.2.1. Distinction from Other Steps
    • 6.5.3.3. Manual Check Against Safety Manuals
    • 6.5.3.4. Inspect Implementation
  • 6.5.4. Dynamic Verification
    • 6.5.4.1. Write Tests
      • 6.5.4.1.1. Tests Derived from Implementation
      • 6.5.4.1.2. Test Cases Can Leverage Contracts
      • 6.5.4.1.3. Testing of Expression Functions
    • 6.5.4.2. Review Tests
    • 6.5.4.3. Formally Verify Test Cases
    • 6.5.4.4. Unit Test Run And Coverage
      • 6.5.4.4.1. Use of Cleanliness-Adjusted ASILs In This Step
    • 6.5.4.5. Handle Coverage Deviations
    • 6.5.4.6. Verify Dynamic Assumptions
      • 6.5.4.6.1. Compiler Switches Outside This Step
      • 6.5.4.6.2. Memory Resource Utilization
      • 6.5.4.6.3. Check Suppressions
  • 6.5.5. Develop Verification Report
• 6.6. Integration Verification
  • 6.6.1. Check Stack Usage (Integration)
    • 6.6.1.1. Approach: Primary Stack Guard Regions
    • 6.6.1.2. Approach: Stack Usage High Water Mark Measurement
    • 6.6.1.3. ASIL of Availability
    • 6.6.1.4. Impact of Compiler Switches
  • 6.6.2. GNATcheck and gnatkp on whole program
  • 6.6.3. Static Analysis (Integration)
  • 6.6.4. Check for Circular Dependencies
  • 6.6.5. Run Integration Tests