Formal Methods

What is Formal Methods about?

  • Small faults in technical systems can have catastrophic consequences (List of famous software bugs)
  • Complexity of systems makes ensuring that the system is correct difficult
  • The aim of formal methods is not…
    • To prove “correctness” of entire systems; its about proving specific properties of systems
    • To replace testing entirely
    • To replace good design practices
  • Formal methods can…
    • Replace (infinitely) many test cases
    • Be used for automatic test case generation
    • Improve the quality of specifications
    • Guarantee specific properties of a specific system model

Terminology

  • Formal Methods is the application of mathematical techniques to the development of “correct” systems
  • Correctness is viewed as two component, validation and verification
  • Validation = “Are we building the right system?” (software fulfills the intended purpose)
  • Verification = “Are we building the system right?” (software meets specifications)
  • Formal Validation is about using logic to ensure that the specification is complete, consistent and accurately captures the requirements
  • Formal Verification is about using logic to ensure that the system is correctly implements its specification
  • Soundness: every statement that is provable is actually true
  • Completeness: every statement that is actually true is provable
  • Automation: proof generation process automatic, semi-automatic or user driven

Limitations of Testing

  • Testing shows the presence of errors but not their absence
  • Choice of test cases is subjective
  • How to test for the unexpected or rare cases?

Limitations of Formal Methods

  • In general it is not feasible to fully specify and verify large software systems
    • Formal methods are usually restricted to important parts of the system and important properties/requirements
  • Just because we have proved something correct does not mean it will actually work
    • There are gaps between the formal verification level and the real-world
    • Does the specification actually capture the intentions?
    • Does the implementation in the real-world behave like the model?

Different Verification Methods

  • Interactive:
    • Theorem Proving#: Relationship between specification and implementation is a theorem in a logic which is proven in the context of a proof calculus
  • Automated:
    • Model Checking: proof of (temporal) logic property (safety & liveness) against a semantic model of the design
    • Invariant Checking (safety property)

References