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 \}) 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 \ 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 \ 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(*>*)