Chapter 5
Model Checking
The future, according to some scientists, will be exactly like the past, only far more expensive.
—John Sladek
In this Chapter, we will:
- [INTRODUCTION] develop the idea of checking the satisfiability of a temporal formula over an appropriate structure (Section 5.1);
- [TECHNIQUE] use Büchi Automata to understand and analyse automated satisfiability checking of temporal formulae, also called model checking (Section 5.2);
- [SYSTEM] examine the Spin system which implements automata-theoretic model checking over execution structures generated from Promela programs (Section 5.3); and
- [ADVANCED] highlight a selection of more advanced work including alternative model-checkers, different logics and extended techniques (Section 5.4).
Again some exercises will be interspersed throughout the chapter with solutions provided in Appendix B.
5.1 Algorithmic Verification
Imagine that we have a temporal formula, φ, that is used to specify some property that we wish to check of a system or component. Now, we have to check this against a description of the component, for example a program. As we have seen, one (deductive) approach is to have another temporal formula, say Γ, that exactly specifies the component (e.g. this formula could be derived via a temporal semantics). Thus, Γ must characterize all the (possibly infinite number of) models (or executions) of the component. To check that the required property holds, we must prove
As we saw earlier, this means establishing ...
