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