For a more extensive introduction we recommend the references given in the preface. In this chapter we introduce the idea of formal specification and verificatio as a 'simple story' along a toy problem.

- A Toy Problem
- Model as Transition Graph
- Model as Execution Graph
- Introducing Properties
- Specification Language CTL
- Finite Automata
- Automaton with Output
- Automaton with Properties
- Model Checking
- Symbolic Model Checking

Gerd Doeben-Henisch 2010-03-03