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

doc-src/TutorialI/CTL/document/Base.tex

author | paulson |

Fri Jan 05 18:32:57 2001 +0100 (2001-01-05) | |

changeset 10795 | 9e888d60d3e5 |

parent 10395 | 7ef380745743 |

child 10867 | bda1701848cd |

permissions | -rw-r--r-- |

minor edits to Chapters 1-3

1 %

2 \begin{isabellebody}%

3 \def\isabellecontext{Base}%

4 %

5 \isamarkupsection{Case study: Verified model checking%

6 }

7 %

8 \begin{isamarkuptext}%

9 \label{sec:VMC}

10 Model checking is a very popular technique for the verification of finite

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

12 (specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic

13 and this section will explore them a little in HOL\@. This is done in two steps: first

14 we consider a simple modal logic called propositional dynamic

15 logic (PDL) which we then extend to the temporal logic CTL used in many real

16 model checkers. In each case we give both a traditional semantics (\isa{{\isasymTurnstile}}) and a

17 recursive function \isa{mc} that maps a formula into the set of all states of

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

19 states, \isa{mc} is directly executable, i.e.\ a model checker, albeit not a

20 very efficient one. The main proof obligation is to show that the semantics

21 and the model checker agree.

23 \underscoreon

25 Our models are \emph{transition systems}, i.e.\ sets of \emph{states} with

26 transitions between them, as shown in this 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

50 state certain \emph{atomic propositions} ($p,q,r$) are true.

51 The aim of temporal logic is to formalize statements such as ``there is no

52 path starting from $s_2$ leading to a state where $p$ or $q$

53 are true'', which is true, and ``on all paths starting from $s_0$ $q$ is always true'',

54 which is false.

56 Abstracting from this concrete example, we assume there is some type of

57 states:%

58 \end{isamarkuptext}%

59 \isacommand{typedecl}\ state%

60 \begin{isamarkuptext}%

61 \noindent

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

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

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

65 because \isa{state} really is an implicit parameter of our model. Of

66 course it would have been more generic to make \isa{state} a type

67 parameter of everything but declaring \isa{state} globally as above

68 reduces clutter. Similarly we declare an arbitrary but fixed

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

70 \end{isamarkuptext}%

71 \isacommand{consts}\ M\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}state\ {\isasymtimes}\ state{\isacharparenright}set{\isachardoublequote}%

72 \begin{isamarkuptext}%

73 \noindent

74 Again, we could have made \isa{M} a parameter of everything.

75 Finally we introduce a type of atomic propositions%

76 \end{isamarkuptext}%

77 \isacommand{typedecl}\ atom%

78 \begin{isamarkuptext}%

79 \noindent

80 and a \emph{labelling function}%

81 \end{isamarkuptext}%

82 \isacommand{consts}\ L\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ atom\ set{\isachardoublequote}%

83 \begin{isamarkuptext}%

84 \noindent

85 telling us which atomic propositions are true in each state.%

86 \end{isamarkuptext}%

87 \end{isabellebody}%

88 %%% Local Variables:

89 %%% mode: latex

90 %%% TeX-master: "root"

91 %%% End: