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: