1 (*<*)theory Base imports Main begin(*>*) |
|
2 |
|
3 section{*Case Study: Verified Model Checking*} |
|
4 |
|
5 text{*\label{sec:VMC} |
|
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 |
|
9 state systems (implementations) with respect to temporal logic formulae |
|
10 (specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are set theoretic |
|
11 and this section will explore them in HOL\@. This is done in two steps. First |
|
12 we consider a simple modal logic called propositional dynamic |
|
13 logic (PDL)\@. We then proceed to the temporal logic CTL, which is |
|
14 used in many real |
|
15 model checkers. In each case we give both a traditional semantics (@{text \<Turnstile>}) and a |
|
16 recursive function @{term mc} that maps a formula into the set of all states of |
|
17 the system where the formula is valid. If the system has a finite number of |
|
18 states, @{term mc} is directly executable: it is a model checker, albeit an |
|
19 inefficient one. The main proof obligation is to show that the semantics |
|
20 and the model checker agree. |
|
21 |
|
22 \underscoreon |
|
23 |
|
24 Our models are \emph{transition systems}:\index{transition systems} |
|
25 sets of \emph{states} with |
|
26 transitions between them. Here is a simple example: |
|
27 \begin{center} |
|
28 \unitlength.5mm |
|
29 \thicklines |
|
30 \begin{picture}(100,60) |
|
31 \put(50,50){\circle{20}} |
|
32 \put(50,50){\makebox(0,0){$p,q$}} |
|
33 \put(61,55){\makebox(0,0)[l]{$s_0$}} |
|
34 \put(44,42){\vector(-1,-1){26}} |
|
35 \put(16,18){\vector(1,1){26}} |
|
36 \put(57,43){\vector(1,-1){26}} |
|
37 \put(10,10){\circle{20}} |
|
38 \put(10,10){\makebox(0,0){$q,r$}} |
|
39 \put(-1,15){\makebox(0,0)[r]{$s_1$}} |
|
40 \put(20,10){\vector(1,0){60}} |
|
41 \put(90,10){\circle{20}} |
|
42 \put(90,10){\makebox(0,0){$r$}} |
|
43 \put(98, 5){\line(1,0){10}} |
|
44 \put(108, 5){\line(0,1){10}} |
|
45 \put(108,15){\vector(-1,0){10}} |
|
46 \put(91,21){\makebox(0,0)[bl]{$s_2$}} |
|
47 \end{picture} |
|
48 \end{center} |
|
49 Each state has a unique name or number ($s_0,s_1,s_2$), and in each state |
|
50 certain \emph{atomic propositions} ($p,q,r$) hold. The aim of temporal logic |
|
51 is to formalize statements such as ``there is no path starting from $s_2$ |
|
52 leading to a state where $p$ or $q$ holds,'' which is true, and ``on all paths |
|
53 starting from $s_0$, $q$ always holds,'' which is false. |
|
54 |
|
55 Abstracting from this concrete example, we assume there is a type of |
|
56 states: |
|
57 *} |
|
58 |
|
59 typedecl state |
|
60 |
|
61 text{*\noindent |
|
62 Command \commdx{typedecl} merely declares a new type but without |
|
63 defining it (see \S\ref{sec:typedecl}). Thus we know nothing |
|
64 about the type other than its existence. That is exactly what we need |
|
65 because @{typ state} really is an implicit parameter of our model. Of |
|
66 course it would have been more generic to make @{typ state} a type |
|
67 parameter of everything but declaring @{typ state} globally as above |
|
68 reduces clutter. Similarly we declare an arbitrary but fixed |
|
69 transition system, i.e.\ a relation between states: |
|
70 *} |
|
71 |
|
72 consts M :: "(state \<times> state)set"; |
|
73 |
|
74 text{*\noindent |
|
75 This is Isabelle's way of declaring a constant without defining it. |
|
76 Finally we introduce a type of atomic propositions |
|
77 *} |
|
78 |
|
79 typedecl "atom" |
|
80 |
|
81 text{*\noindent |
|
82 and a \emph{labelling function} |
|
83 *} |
|
84 |
|
85 consts L :: "state \<Rightarrow> atom set" |
|
86 |
|
87 text{*\noindent |
|
88 telling us which atomic propositions are true in each state. |
|
89 *} |
|
90 |
|
91 (*<*)end(*>*) |
|