# 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:
• : 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)