17914

1 
(*<*)theory Base imports Main begin(*>*)

10123

2 

10867

3 
section{*Case Study: Verified Model Checking*}

10123

4 

10362

5 
text{*\label{sec:VMC}

10867

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

10795

9 
state systems (implementations) with respect to temporal logic formulae

10867

10 
(specifications) \cite{ClarkeGPbook,HuthRyanbook}. Its foundations are set theoretic


11 
and this section will explore them in HOL\@. This is done in two steps. First

10178

12 
we consider a simple modal logic called propositional dynamic

11458

13 
logic (PDL)\@. We then proceed to the temporal logic CTL, which is

10867

14 
used in many real

10123

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

10867

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

10123

20 
and the model checker agree.


21 

10133

22 
\underscoreon

10123

23 

11458

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:

10133

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}

11458

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.

10123

54 

11458

55 
Abstracting from this concrete example, we assume there is a type of

10281

56 
states:

10123

57 
*}


58 

10133

59 
typedecl state

10123

60 


61 
text{*\noindent

11458

62 
Command \commdx{typedecl} merely declares a new type but without

10983

63 
defining it (see \S\ref{sec:typedecl}). Thus we know nothing

10281

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

10867

69 
transition system, i.e.\ a relation between states:

10123

70 
*}


71 


72 
consts M :: "(state \<times> state)set";


73 


74 
text{*\noindent

27015

75 
This is Isabelle's way of declaring a constant without defining it.

10133

76 
Finally we introduce a type of atomic propositions

10123

77 
*}

10133

78 

18724

79 
typedecl "atom"

10133

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 

10123

91 
(*<*)end(*>*)
