src/Doc/Tutorial/CTL/Base.thy
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;
wenzelm@17914
     1
(*<*)theory Base imports Main begin(*>*)
nipkow@10123
     2
paulson@10867
     3
section{*Case Study: Verified Model Checking*}
nipkow@10123
     4
nipkow@10362
     5
text{*\label{sec:VMC}
paulson@10867
     6
This chapter ends with a case study concerning model checking for 
paulson@10867
     7
Computation Tree Logic (CTL), a temporal logic.
paulson@10867
     8
Model checking is a popular technique for the verification of finite
paulson@10795
     9
state systems (implementations) with respect to temporal logic formulae
wenzelm@58620
    10
(specifications) @{cite "ClarkeGP-book" and "Huth-Ryan-book"}. Its foundations are set theoretic
paulson@10867
    11
and this section will explore them in HOL\@. This is done in two steps.  First
nipkow@10178
    12
we consider a simple modal logic called propositional dynamic
paulson@11458
    13
logic (PDL)\@.  We then proceed to the temporal logic CTL, which is
paulson@10867
    14
used in many real
nipkow@10123
    15
model checkers. In each case we give both a traditional semantics (@{text \<Turnstile>}) and a
nipkow@10123
    16
recursive function @{term mc} that maps a formula into the set of all states of
nipkow@10123
    17
the system where the formula is valid. If the system has a finite number of
paulson@10867
    18
states, @{term mc} is directly executable: it is a model checker, albeit an
paulson@10867
    19
inefficient one. The main proof obligation is to show that the semantics
nipkow@10123
    20
and the model checker agree.
nipkow@10123
    21
nipkow@10133
    22
\underscoreon
nipkow@10123
    23
paulson@11458
    24
Our models are \emph{transition systems}:\index{transition systems}
paulson@11458
    25
sets of \emph{states} with
paulson@11458
    26
transitions between them.  Here is a 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}
paulson@11458
    49
Each state has a unique name or number ($s_0,s_1,s_2$), and in each state
paulson@11458
    50
certain \emph{atomic propositions} ($p,q,r$) hold.  The aim of temporal logic
paulson@11458
    51
is to formalize statements such as ``there is no path starting from $s_2$
paulson@11458
    52
leading to a state where $p$ or $q$ holds,'' which is true, and ``on all paths
paulson@11458
    53
starting from $s_0$, $q$ always holds,'' which is false.
nipkow@10123
    54
paulson@11458
    55
Abstracting from this concrete example, we assume there is a type of
nipkow@10281
    56
states:
nipkow@10123
    57
*}
nipkow@10123
    58
nipkow@10133
    59
typedecl state
nipkow@10123
    60
nipkow@10123
    61
text{*\noindent
paulson@11458
    62
Command \commdx{typedecl} merely declares a new type but without
nipkow@10983
    63
defining it (see \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 @{typ state} really is an implicit parameter of our model.  Of
nipkow@10281
    66
course it would have been more generic to make @{typ state} a type
nipkow@10281
    67
parameter of everything but declaring @{typ state} globally as above
nipkow@10281
    68
reduces clutter.  Similarly we declare an arbitrary but fixed
paulson@10867
    69
transition system, i.e.\ a relation between states:
nipkow@10123
    70
*}
nipkow@10123
    71
wenzelm@58860
    72
consts M :: "(state \<times> state)set"
nipkow@10123
    73
nipkow@10123
    74
text{*\noindent
nipkow@27015
    75
This is Isabelle's way of declaring a constant without defining it.
nipkow@10133
    76
Finally we introduce a type of atomic propositions
nipkow@10123
    77
*}
nipkow@10133
    78
wenzelm@18724
    79
typedecl "atom"
nipkow@10133
    80
nipkow@10133
    81
text{*\noindent
nipkow@10133
    82
and a \emph{labelling function}
nipkow@10133
    83
*}
nipkow@10133
    84
nipkow@10133
    85
consts L :: "state \<Rightarrow> atom set"
nipkow@10133
    86
nipkow@10133
    87
text{*\noindent
nipkow@10133
    88
telling us which atomic propositions are true in each state.
nipkow@10133
    89
*}
nipkow@10133
    90
nipkow@10123
    91
(*<*)end(*>*)