author wenzelm
Sat Nov 01 14:20:38 2014 +0100 (2014-11-01)
changeset 58860 fee7cfa69c50
parent 58620 7435b6a3f72e
child 67406 23307fd33906
permissions -rw-r--r--
eliminated spurious semicolons;
     1 (*<*)theory Base imports Main begin(*>*)
     3 section{*Case Study: Verified Model Checking*}
     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" and "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.
    22 \underscoreon
    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.
    55 Abstracting from this concrete example, we assume there is a type of
    56 states:
    57 *}
    59 typedecl state
    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 *}
    72 consts M :: "(state \<times> state)set"
    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 *}
    79 typedecl "atom"
    81 text{*\noindent
    82 and a \emph{labelling function}
    83 *}
    85 consts L :: "state \<Rightarrow> atom set"
    87 text{*\noindent
    88 telling us which atomic propositions are true in each state.
    89 *}
    91 (*<*)end(*>*)