# Formal Methods

- 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?

- 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