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