9. Formal Verification

• 9.1. Formal Verification Overview
• 9.2. Formal Verification Approaches
  • 9.2.1. Formal Methods Overview
  • 9.2.2. Formal Methods actively considered
    • 9.2.2.1. Frama-C
    • 9.2.2.2. Isabelle/HOL
  • 9.2.3. Formal Method actually used
    • 9.2.3.1. Promela/SPIN
• 9.3. Test Generation Methodology
  • 9.3.1. Model desired behavior
  • 9.3.2. Make claims about undesired behavior
  • 9.3.3. Map good behavior scenarios to tests
• 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