Skip to main content
Ctrl+K

6.17c582f

  • 1. Preface
  • 2. RTEMS Project Mission Statement
  • 3. RTEMS Stakeholders
  • 4. Introduction to Pre-Qualification
  • 5. Software Requirements Engineering
    • 5.1. Requirements for Requirements
    • 5.2. Specification Items
    • 5.3. Traceability of Specification Items
    • 5.4. Requirement Management
    • 5.5. Tooling
    • 5.6. How-To
  • 6. Software Development Management
    • 6.1. Software Development (Git Users)
    • 6.2. Software Development (Git Writers)
    • 6.3. Coding Standards
      • 6.3.1. Coding Conventions
      • 6.3.2. Formatting
      • 6.3.3. Deprectating Interfaces
      • 6.3.4. Doxygen Guidelines
      • 6.3.5. File Templates
      • 6.3.6. Naming Rules
    • 6.4. Documentation Guidelines
    • 6.5. Python Development Guidelines
    • 6.6. Change Management
    • 6.7. Issue Tracking
  • 7. Software Test Plan Assurance and Procedures
    • 7.1.1. Test Suites
    • 7.1.2. RTEMS Tester
  • 8. Software Test Framework
  • 9. Formal Verification
    • 9.1. Formal Verification Overview
    • 9.2. Formal Verification Approaches
    • 9.3. Test Generation Methodology
    • 9.4. Formal Tools Setup
    • 9.5. Modelling with Promela
    • 9.6. Promela to C Refinement
  • 10. BSP Build System
  • 11. Software Release Management
    • 11.1. Release Process
    • 11.2. Release Maintenance
    • 11.3. Software Change Report Generation
    • 11.4. Version Description Document (VDD) Generation
  • 12. User’s Manuals
  • 13. Licensing Requirements
  • 14. Appendix: Core Qualification Artifacts/Documents
  • 15. Appendix: RTEMS Formal Model Guide
  • 16. Glossary
  • 17. References
  • Repository
  • Show source
  • Suggest edit
  • Open issue
  • .rst

  • 9.4. Formal Tools Setup
    • 9.4.1. Installing Tools
      • 9.4.1.1. Installing Promela/SPIN
      • 9.4.1.2. Installing Test Generation Tools
    • 9.4.2. Tool Configuration
      • 9.4.2.1. Testsuite Setup
    • 9.4.3. Running Test Generation
  • 9.5. Modelling with Promela
    • 9.5.1. Promela Execution
      • 9.5.1.1. Simulation vs. Verification
    • 9.5.2. Promela Datatypes
    • 9.5.3. Promela Declarations
      • 9.5.3.1. Special Identifiers
    • 9.5.4. Promela Atomic Statements
    • 9.5.5. Promela Composite Statements
    • 9.5.6. Promela Top-Level
  • 9.6. Promela to C Refinement
    • 9.6.1. Model Annotations
      • 9.6.1.1. Annotation Syntax
    • 9.6.2. Annotation Lookup
    • 9.6.3. Specifying Refinement
      • 9.6.3.1. Lookup Example
    • 9.6.4. Annotation Refinement Guide
      • 9.6.4.1. LOG
      • 9.6.4.2. NAME
      • 9.6.4.3. INIT
      • 9.6.4.4. TASK
      • 9.6.4.5. SIGNAL
      • 9.6.4.6. WAIT
      • 9.6.4.7. DEF
      • 9.6.4.8. DECL
      • 9.6.4.9. DCLARRAY
      • 9.6.4.10. CALL
      • 9.6.4.11. STATE
      • 9.6.4.12. STRUCT
      • 9.6.4.13. SEQ
      • 9.6.4.14. PTR
      • 9.6.4.15. SCALAR
      • 9.6.4.16. END
      • 9.6.4.17. SUSPEND and WAKEUP
    • 9.6.5. Annotation Ordering
    • 9.6.6. Test Code Assembly
      • 9.6.6.1. Scenario Generation
      • 9.6.6.2. Test Code Generation
      • 9.6.6.3. Test Code Deployment
      • 9.6.6.4. Performing Tests
    • 9.6.7. Traceability

previous

9.3. Test Generation Methodology

next

9.4. Formal Tools Setup

By RTEMS Project

© Copyright 1988-2024 RTEMS Project and contributors.

Last updated on Nov 27, 2024.