summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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;

1 (*<*)theory Base imports Main begin(*>*)

3 section{*Case Study: Verified Model Checking*}

5 text{*\label{sec:VMC}

6 This chapter ends with a case study concerning model checking for

7 Computation Tree Logic (CTL), a temporal logic.

8 Model checking is a popular technique for the verification of finite

9 state systems (implementations) with respect to temporal logic formulae

10 (specifications) @{cite "ClarkeGP-book" and "Huth-Ryan-book"}. Its foundations are set theoretic

11 and this section will explore them in HOL\@. This is done in two steps. First

12 we consider a simple modal logic called propositional dynamic

13 logic (PDL)\@. We then proceed to the temporal logic CTL, which is

14 used in many real

15 model checkers. In each case we give both a traditional semantics (@{text \<Turnstile>}) and a

16 recursive function @{term mc} that maps a formula into the set of all states of

17 the system where the formula is valid. If the system has a finite number of

18 states, @{term mc} is directly executable: it is a model checker, albeit an

19 inefficient one. The main proof obligation is to show that the semantics

20 and the model checker agree.

22 \underscoreon

24 Our models are \emph{transition systems}:\index{transition systems}

25 sets of \emph{states} with

26 transitions between them. Here is a simple example:

27 \begin{center}

28 \unitlength.5mm

29 \thicklines

30 \begin{picture}(100,60)

31 \put(50,50){\circle{20}}

32 \put(50,50){\makebox(0,0){$p,q$}}

33 \put(61,55){\makebox(0,0)[l]{$s_0$}}

34 \put(44,42){\vector(-1,-1){26}}

35 \put(16,18){\vector(1,1){26}}

36 \put(57,43){\vector(1,-1){26}}

37 \put(10,10){\circle{20}}

38 \put(10,10){\makebox(0,0){$q,r$}}

39 \put(-1,15){\makebox(0,0)[r]{$s_1$}}

40 \put(20,10){\vector(1,0){60}}

41 \put(90,10){\circle{20}}

42 \put(90,10){\makebox(0,0){$r$}}

43 \put(98, 5){\line(1,0){10}}

44 \put(108, 5){\line(0,1){10}}

45 \put(108,15){\vector(-1,0){10}}

46 \put(91,21){\makebox(0,0)[bl]{$s_2$}}

47 \end{picture}

48 \end{center}

49 Each state has a unique name or number ($s_0,s_1,s_2$), and in each state

50 certain \emph{atomic propositions} ($p,q,r$) hold. The aim of temporal logic

51 is to formalize statements such as ``there is no path starting from $s_2$

52 leading to a state where $p$ or $q$ holds,'' which is true, and ``on all paths

53 starting from $s_0$, $q$ always holds,'' which is false.

55 Abstracting from this concrete example, we assume there is a type of

56 states:

57 *}

59 typedecl state

61 text{*\noindent

62 Command \commdx{typedecl} merely declares a new type but without

63 defining it (see \S\ref{sec:typedecl}). Thus we know nothing

64 about the type other than its existence. That is exactly what we need

65 because @{typ state} really is an implicit parameter of our model. Of

66 course it would have been more generic to make @{typ state} a type

67 parameter of everything but declaring @{typ state} globally as above

68 reduces clutter. Similarly we declare an arbitrary but fixed

69 transition system, i.e.\ a relation between states:

70 *}

72 consts M :: "(state \<times> state)set"

74 text{*\noindent

75 This is Isabelle's way of declaring a constant without defining it.

76 Finally we introduce a type of atomic propositions

77 *}

79 typedecl "atom"

81 text{*\noindent

82 and a \emph{labelling function}

83 *}

85 consts L :: "state \<Rightarrow> atom set"

87 text{*\noindent

88 telling us which atomic propositions are true in each state.

89 *}

91 (*<*)end(*>*)