Formal methods

File size
7.3KB
Lines of code
147

Formal methods

  • Mathematically prove or disprove the correctness of a system's design and behaviour according to formal specifications
  • Shows both the presence and absence of specific errors
  • For language design, software, hardware, algorithms

Quickstart

Formal methods comprise the following 2 steps

  1. Specification

    • Describe the desired properties (and behaviors) of a system
    • Written in formal languages
      1. Tempora logic: specifies properties of systems that evolve over time
      2. Algebraic specification: defines abstract datatypes and their operations

  2. Verification

    1. Model checking
      • System is modelled as a finite state model
      • Exhaustively explores whether user-specified properties (expressed in temporal logic) hold in every possible model state
      • Suitable for hardware verification and concurrent systems
        1. SPIN: widely-used model checker for verifying the correctness of distributed software models
        2. NuSMV: symbolic model checker supporting both BDD-based and SAT-based verification
      • Pros
        • fully automated
        • able to handle concurrent systems
        • produces counterexamples when a given property does NOT hold
      • Cons
        • suffers from State Space Explosion (as a system grows, the number of states becomes unmanageably large)
        • limited to finite state systems
    2. Theorem proving
      • System is described in a formal language
        1. Z Notation: used for describing the structure and behavior of software, particularly in safety-critical and high-assurance systems
        2. TLA+: used for reasoning about concurrent and distributed systems, enabling precise descriptions of software system behaviors
        3. Alloy: lightweight modeling language for specifying complex structures and constraints in software systems
        4. VDM: Vienna Development Method is a formal method that provides a set of modeling languages for specifying and verifying software systems in the early stages of design
        5. VHDL: VHSIC Hardware Description Language describes the behavior and structure of electronic systems, commonly used in the design and simulation of digital circuits and hardware components
        6. Verilog: hardware description language for modeling electronic systems at various levels of abstraction from gate level to system-level
        7. PVS: Prototype Verification System used for formal specification and verification of algorithm in areas like automated reasoning
        8. Coq: formal language and proof assistant for developing and verifying mathematical proofs and algorithms, particularly in functional programming and theorem proving
        9. Isabelle: generic proof assistant used for formal verification of both software and hardware systems
    3. Symbolic execution
      • Program is executed with symbolic inputs instead of literal values
      • Explores multiple execution paths simultaneously
        1. KLEE: symbolic execution tool that automatically generates high-coverage tests
      • Pros
        • capable of analyzing ALL possible execution paths in a program
        • finds bugs in code WITHOUT requiring a full formal specification
        • checks for errors like division by zero or buffer overflows
      • Cons
        • suffers from Path Explosion (as program complexity grows, the number of paths quickly becomes unmanageably large)
        • limited to certain types of errors

More on