1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{Base}% |
3 \def\isabellecontext{Base}% |
4 % |
4 % |
5 \isamarkupsection{Case study: Verified model checkers} |
5 \isamarkupsection{Case study: Verified model checking} |
6 % |
6 % |
7 \begin{isamarkuptext}% |
7 \begin{isamarkuptext}% |
8 Model checking is a very popular technique for the verification of finite |
8 Model checking is a very popular technique for the verification of finite |
9 state systems (implementations) w.r.t.\ temporal logic formulae |
9 state systems (implementations) w.r.t.\ temporal logic formulae |
10 (specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic |
10 (specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic |
50 path starting from $s_2$ leading to a state where $p$ or $q$ |
50 path starting from $s_2$ leading to a state where $p$ or $q$ |
51 are true'', which is true, and ``on all paths starting from $s_0$ $q$ is always true'', |
51 are true'', which is true, and ``on all paths starting from $s_0$ $q$ is always true'', |
52 which is false. |
52 which is false. |
53 |
53 |
54 Abstracting from this concrete example, we assume there is some type of |
54 Abstracting from this concrete example, we assume there is some type of |
55 states% |
55 states:% |
56 \end{isamarkuptext}% |
56 \end{isamarkuptext}% |
57 \isacommand{typedecl}\ state% |
57 \isacommand{typedecl}\ state% |
58 \begin{isamarkuptext}% |
58 \begin{isamarkuptext}% |
59 \noindent |
59 \noindent |
60 which we merely declare rather than define because it is an implicit |
60 Command \isacommand{typedecl} merely declares a new type but without |
61 parameter of our model. Of course it would have been more generic to make |
61 defining it (see also \S\ref{sec:typedecl}). Thus we know nothing |
62 \isa{state} a type parameter of everything but fixing \isa{state} as above |
62 about the type other than its existence. That is exactly what we need |
63 reduces clutter. |
63 because \isa{state} really is an implicit parameter of our model. Of |
64 Similarly we declare an arbitrary but fixed transition system, i.e.\ |
64 course it would have been more generic to make \isa{state} a type |
65 relation between states:% |
65 parameter of everything but declaring \isa{state} globally as above |
|
66 reduces clutter. Similarly we declare an arbitrary but fixed |
|
67 transition system, i.e.\ relation between states:% |
66 \end{isamarkuptext}% |
68 \end{isamarkuptext}% |
67 \isacommand{consts}\ M\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}state\ {\isasymtimes}\ state{\isacharparenright}set{\isachardoublequote}% |
69 \isacommand{consts}\ M\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}state\ {\isasymtimes}\ state{\isacharparenright}set{\isachardoublequote}% |
68 \begin{isamarkuptext}% |
70 \begin{isamarkuptext}% |
69 \noindent |
71 \noindent |
70 Again, we could have made \isa{M} a parameter of everything. |
72 Again, we could have made \isa{M} a parameter of everything. |