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