author wenzelm
Mon, 07 Oct 2013 21:24:44 +0200
changeset 54313 da2e6282a4f5
parent 48985 5386df44a037
child 58620 7435b6a3f72e
permissions -rw-r--r--
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;

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

section{*Case Study: Verified Model Checking*}

This chapter ends with a case study concerning model checking for 
Computation Tree Logic (CTL), a temporal logic.
Model checking is a popular technique for the verification of finite
state systems (implementations) with respect to temporal logic formulae
(specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are set theoretic
and this section will explore them in HOL\@. This is done in two steps.  First
we consider a simple modal logic called propositional dynamic
logic (PDL)\@.  We then proceed to the temporal logic CTL, which is
used in many real
model checkers. In each case we give both a traditional semantics (@{text \<Turnstile>}) and a
recursive function @{term mc} that maps a formula into the set of all states of
the system where the formula is valid. If the system has a finite number of
states, @{term mc} is directly executable: it is a model checker, albeit an
inefficient one. The main proof obligation is to show that the semantics
and the model checker agree.


Our models are \emph{transition systems}:\index{transition systems}
sets of \emph{states} with
transitions between them.  Here is a simple example:
\put(98, 5){\line(1,0){10}}
\put(108, 5){\line(0,1){10}}
Each state has a unique name or number ($s_0,s_1,s_2$), and in each state
certain \emph{atomic propositions} ($p,q,r$) hold.  The aim of temporal logic
is to formalize statements such as ``there is no path starting from $s_2$
leading to a state where $p$ or $q$ holds,'' which is true, and ``on all paths
starting from $s_0$, $q$ always holds,'' which is false.

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

typedecl state

Command \commdx{typedecl} merely declares a new type but without
defining it (see \S\ref{sec:typedecl}). Thus we know nothing
about the type other than its existence. That is exactly what we need
because @{typ state} really is an implicit parameter of our model.  Of
course it would have been more generic to make @{typ state} a type
parameter of everything but declaring @{typ state} globally as above
reduces clutter.  Similarly we declare an arbitrary but fixed
transition system, i.e.\ a relation between states:

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

This is Isabelle's way of declaring a constant without defining it.
Finally we introduce a type of atomic propositions

typedecl "atom"

and a \emph{labelling function}

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

telling us which atomic propositions are true in each state.