1 (*<*)theory Base = Main:(*>*) |
1 (*<*)theory Base = Main:(*>*) |
2 |
2 |
3 section{*Case study: Verified model checking*} |
3 section{*Case Study: Verified Model Checking*} |
4 |
4 |
5 text{*\label{sec:VMC} |
5 text{*\label{sec:VMC} |
6 Model checking is a very popular technique for the verification of finite |
6 This chapter ends with a case study concerning model checking for |
|
7 Computation Tree Logic (CTL), a temporal logic. |
|
8 Model checking is a popular technique for the verification of finite |
7 state systems (implementations) with respect to temporal logic formulae |
9 state systems (implementations) with respect to temporal logic formulae |
8 (specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic |
10 (specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are set theoretic |
9 and this section will explore them a little in HOL\@. This is done in two steps: first |
11 and this section will explore them in HOL\@. This is done in two steps. First |
10 we consider a simple modal logic called propositional dynamic |
12 we consider a simple modal logic called propositional dynamic |
11 logic (PDL) which we then extend to the temporal logic CTL used in many real |
13 logic (PDL), which we then extend to the temporal logic CTL, which is |
|
14 used in many real |
12 model checkers. In each case we give both a traditional semantics (@{text \<Turnstile>}) and a |
15 model checkers. In each case we give both a traditional semantics (@{text \<Turnstile>}) and a |
13 recursive function @{term mc} that maps a formula into the set of all states of |
16 recursive function @{term mc} that maps a formula into the set of all states of |
14 the system where the formula is valid. If the system has a finite number of |
17 the system where the formula is valid. If the system has a finite number of |
15 states, @{term mc} is directly executable, i.e.\ a model checker, albeit not a |
18 states, @{term mc} is directly executable: it is a model checker, albeit an |
16 very efficient one. The main proof obligation is to show that the semantics |
19 inefficient one. The main proof obligation is to show that the semantics |
17 and the model checker agree. |
20 and the model checker agree. |
18 |
21 |
19 \underscoreon |
22 \underscoreon |
20 |
23 |
21 Our models are \emph{transition systems}, i.e.\ sets of \emph{states} with |
24 Our models are \emph{transition systems}, i.e.\ sets of \emph{states} with |
61 about the type other than its existence. That is exactly what we need |
64 about the type other than its existence. That is exactly what we need |
62 because @{typ state} really is an implicit parameter of our model. Of |
65 because @{typ state} really is an implicit parameter of our model. Of |
63 course it would have been more generic to make @{typ state} a type |
66 course it would have been more generic to make @{typ state} a type |
64 parameter of everything but declaring @{typ state} globally as above |
67 parameter of everything but declaring @{typ state} globally as above |
65 reduces clutter. Similarly we declare an arbitrary but fixed |
68 reduces clutter. Similarly we declare an arbitrary but fixed |
66 transition system, i.e.\ relation between states: |
69 transition system, i.e.\ a relation between states: |
67 *} |
70 *} |
68 |
71 |
69 consts M :: "(state \<times> state)set"; |
72 consts M :: "(state \<times> state)set"; |
70 |
73 |
71 text{*\noindent |
74 text{*\noindent |