doc-src/TutorialI/CTL/document/Base.tex
 author nipkow Wed Dec 06 13:22:58 2000 +0100 (2000-12-06) changeset 10608 620647438780 parent 10395 7ef380745743 child 10795 9e888d60d3e5 permissions -rw-r--r--
*** empty log message ***
 nipkow@10123  1 %  nipkow@10123  2 \begin{isabellebody}%  nipkow@10123  3 \def\isabellecontext{Base}%  nipkow@10123  4 %  wenzelm@10395  5 \isamarkupsection{Case study: Verified model checking%  wenzelm@10395  6 }  nipkow@10123  7 %  nipkow@10123  8 \begin{isamarkuptext}%  nipkow@10362  9 \label{sec:VMC}  nipkow@10123  10 Model checking is a very popular technique for the verification of finite  nipkow@10123  11 state systems (implementations) w.r.t.\ temporal logic formulae  nipkow@10192  12 (specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic  nipkow@10186  13 and this section shall explore them a little in HOL. This is done in two steps: first  nipkow@10178  14 we consider a simple modal logic called propositional dynamic  nipkow@10123  15 logic (PDL) which we then extend to the temporal logic CTL used in many real  nipkow@10123  16 model checkers. In each case we give both a traditional semantics (\isa{{\isasymTurnstile}}) and a  nipkow@10123  17 recursive function \isa{mc} that maps a formula into the set of all states of  nipkow@10123  18 the system where the formula is valid. If the system has a finite number of  nipkow@10123  19 states, \isa{mc} is directly executable, i.e.\ a model checker, albeit not a  nipkow@10123  20 very efficient one. The main proof obligation is to show that the semantics  nipkow@10123  21 and the model checker agree.  nipkow@10123  22 nipkow@10133  23 \underscoreon  nipkow@10123  24 nipkow@10133  25 Our models are \emph{transition systems}, i.e.\ sets of \emph{states} with  nipkow@10133  26 transitions between them, as shown in this simple example:  nipkow@10133  27 \begin{center}  nipkow@10133  28 \unitlength.5mm  nipkow@10133  29 \thicklines  nipkow@10133  30 \begin{picture}(100,60)  nipkow@10133  31 \put(50,50){\circle{20}}  nipkow@10133  32 \put(50,50){\makebox(0,0){$p,q$}}  nipkow@10133  33 \put(61,55){\makebox(0,0)[l]{$s_0$}}  nipkow@10133  34 \put(44,42){\vector(-1,-1){26}}  nipkow@10133  35 \put(16,18){\vector(1,1){26}}  nipkow@10133  36 \put(57,43){\vector(1,-1){26}}  nipkow@10133  37 \put(10,10){\circle{20}}  nipkow@10133  38 \put(10,10){\makebox(0,0){$q,r$}}  nipkow@10133  39 \put(-1,15){\makebox(0,0)[r]{$s_1$}}  nipkow@10133  40 \put(20,10){\vector(1,0){60}}  nipkow@10133  41 \put(90,10){\circle{20}}  nipkow@10133  42 \put(90,10){\makebox(0,0){$r$}}  nipkow@10133  43 \put(98, 5){\line(1,0){10}}  nipkow@10133  44 \put(108, 5){\line(0,1){10}}  nipkow@10133  45 \put(108,15){\vector(-1,0){10}}  nipkow@10133  46 \put(91,21){\makebox(0,0)[bl]{$s_2$}}  nipkow@10133  47 \end{picture}  nipkow@10133  48 \end{center}  nipkow@10133  49 Each state has a unique name or number ($s_0,s_1,s_2$), and in each  nipkow@10133  50 state certain \emph{atomic propositions} ($p,q,r$) are true.  nipkow@10133  51 The aim of temporal logic is to formalize statements such as there is no  nipkow@10186  52 path starting from $s_2$ leading to a state where $p$ or $q$  nipkow@10186  53 are true'', which is true, and on all paths starting from $s_0$ $q$ is always true'',  nipkow@10186  54 which is false.  nipkow@10123  55 nipkow@10123  56 Abstracting from this concrete example, we assume there is some type of  nipkow@10281  57 states:%  nipkow@10133  58 \end{isamarkuptext}%  nipkow@10133  59 \isacommand{typedecl}\ state%  nipkow@10133  60 \begin{isamarkuptext}%  nipkow@10133  61 \noindent  nipkow@10281  62 Command \isacommand{typedecl} merely declares a new type but without  nipkow@10281  63 defining it (see also \S\ref{sec:typedecl}). Thus we know nothing  nipkow@10281  64 about the type other than its existence. That is exactly what we need  nipkow@10281  65 because \isa{state} really is an implicit parameter of our model. Of  nipkow@10281  66 course it would have been more generic to make \isa{state} a type  nipkow@10281  67 parameter of everything but declaring \isa{state} globally as above  nipkow@10281  68 reduces clutter. Similarly we declare an arbitrary but fixed  nipkow@10281  69 transition system, i.e.\ relation between states:%  nipkow@10133  70 \end{isamarkuptext}%  nipkow@10133  71 \isacommand{consts}\ M\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}state\ {\isasymtimes}\ state{\isacharparenright}set{\isachardoublequote}%  nipkow@10133  72 \begin{isamarkuptext}%  nipkow@10133  73 \noindent  nipkow@10133  74 Again, we could have made \isa{M} a parameter of everything.  nipkow@10133  75 Finally we introduce a type of atomic propositions%  nipkow@10123  76 \end{isamarkuptext}%  nipkow@10123  77 \isacommand{typedecl}\ atom%  nipkow@10123  78 \begin{isamarkuptext}%  nipkow@10123  79 \noindent  nipkow@10133  80 and a \emph{labelling function}%  nipkow@10123  81 \end{isamarkuptext}%  nipkow@10133  82 \isacommand{consts}\ L\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ atom\ set{\isachardoublequote}%  nipkow@10123  83 \begin{isamarkuptext}%  nipkow@10123  84 \noindent  nipkow@10133  85 telling us which atomic propositions are true in each state.%  nipkow@10123  86 \end{isamarkuptext}%  nipkow@10123  87 \end{isabellebody}%  nipkow@10123  88 %%% Local Variables:  nipkow@10123  89 %%% mode: latex  nipkow@10123  90 %%% TeX-master: "root"  nipkow@10123  91 %%% End: