Rigorous Firmware Development

The following sections are included:

• Specification Based Function Block Development

• Formalising Requirements

  • Problem Statement

  • Requirements Specifications

  • OBJ

  • Functional Requirements of nonlin

• Design Specification of Function Block nonlin

• Specification Verification

  • Inductive Proofs with Equations

  • Correctness of Function f'

• Specification Testing

• Program Verification

  • A Subset of Structured Text: Simple ST

  • Weakest Preconditions

  • Correctness of Program nonlin

• A Second Example

  • Problem Statement

  • Functional Requirements of check

  • Design of check

  • Correctness of Functions cond, ua, and la

  • ST Program Implementing Function Block check

  • Hoare Style Proof Rules

  • Correctness of Program check

  • Improvement of Program check

• Verification of a Timer Program using HOL

  • Abstract Syntax of Simple ST

  • Semantics of Simple ST in HOL

  • Timer Verification

• Summary