author wenzelm
Sat Nov 04 18:54:22 2000 +0100 (2000-11-04)
changeset 10395 7ef380745743
parent 10362 c6b197ccf1f1
child 10795 9e888d60d3e5
permissions -rw-r--r--
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Base}%
     4 %
     5 \isamarkupsection{Case study: Verified model checking%
     6 }
     7 %
     8 \begin{isamarkuptext}%
     9 \label{sec:VMC}
    10 Model checking is a very popular technique for the verification of finite
    11 state systems (implementations) w.r.t.\ temporal logic formulae
    12 (specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic
    13 and this section shall explore them a little in HOL. This is done in two steps: first
    14 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
    16 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
    18 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
    20 very efficient one. The main proof obligation is to show that the semantics
    21 and the model checker agree.
    23 \underscoreon
    25 Our models are \emph{transition systems}, i.e.\ sets of \emph{states} with
    26 transitions between them, as shown in this 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
    50 state certain \emph{atomic propositions} ($p,q,r$) are true.
    51 The aim of temporal logic is to formalize statements such as ``there is no
    52 path starting from $s_2$ leading to a state where $p$ or $q$
    53 are true'', which is true, and ``on all paths starting from $s_0$ $q$ is always true'',
    54 which is false.
    56 Abstracting from this concrete example, we assume there is some type of
    57 states:%
    58 \end{isamarkuptext}%
    59 \isacommand{typedecl}\ state%
    60 \begin{isamarkuptext}%
    61 \noindent
    62 Command \isacommand{typedecl} merely declares a new type but without
    63 defining it (see also \S\ref{sec:typedecl}). Thus we know nothing
    64 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
    66 course it would have been more generic to make \isa{state} a type
    67 parameter of everything but declaring \isa{state} globally as above
    68 reduces clutter.  Similarly we declare an arbitrary but fixed
    69 transition system, i.e.\ relation between states:%
    70 \end{isamarkuptext}%
    71 \isacommand{consts}\ M\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}state\ {\isasymtimes}\ state{\isacharparenright}set{\isachardoublequote}%
    72 \begin{isamarkuptext}%
    73 \noindent
    74 Again, we could have made \isa{M} a parameter of everything.
    75 Finally we introduce a type of atomic propositions%
    76 \end{isamarkuptext}%
    77 \isacommand{typedecl}\ atom%
    78 \begin{isamarkuptext}%
    79 \noindent
    80 and a \emph{labelling function}%
    81 \end{isamarkuptext}%
    82 \isacommand{consts}\ L\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ atom\ set{\isachardoublequote}%
    83 \begin{isamarkuptext}%
    84 \noindent
    85 telling us which atomic propositions are true in each state.%
    86 \end{isamarkuptext}%
    87 \end{isabellebody}%
    88 %%% Local Variables:
    89 %%% mode: latex
    90 %%% TeX-master: "root"
    91 %%% End: