35 This is a brief description of the \hc{}\index{holCheckLib!\hc{}} model checker, version 1.0. It assumes the reader is familiar with symbolic model checking, with \HOL{}, and, ideally, with \texttt{HolBddLib}, the \HOL{} interface to BDDs. It should be read with a working \HOL{} installation at hand.
39 \hc{} is a BDD-based model checker embedded in the \HOL{} theorem prover, interfaced to an external BDD engine for efficiency. It currently has the following features:
42 \item All steps of the algorithm are proved in \HOL{}, with BDD operations considered atomic.
43 \item Results are returned as \HOL{} theorems.
59 See \S\ref{sec:models} for details. The user is required to supply only \( S_0 \) and \( T \) as the remaining components can be calculated from these. Properties are input as \HOL{} terms of type \(\mathtt{mu}\) or \(\mathtt{ctl}\), \HOL{} datatypes for which have been defined (see \S\ref{sec:prop} for details). A property is satisfied by a model if the set of initial states of the model is a subset of the set of states satisfying the property.
183 For our running example, we use \texttt{ttt.sml} from \texttt{src/HolCheck/examples}. Build this (and others\footnote{The AMBA examples are large and take a while to build. To skip them, see the README file in the same folder.}) by typing \texttt{Holmake} in \texttt{src/HolCheck/examples}. Now start \HOL{} from this directory (or use the -I command-line parameter).
185 The first step after loading \HOL{} is to load \hc{}. \HOL{} messages have been elided.
236 \(\mathtt{TS}\) is a list of pairs of the form \( (a,R_a)\), where the string \(a\) is an action name (or transition label) and the \HOL{} term \(R_a\) is a relation over current and next states such that the model has a transition labelled \(a\) from a state \( s \) to a state \(s'\) if and only if the corresponding valuations of current and next state variables satisfy \( R_a \). In this example, there are two actions, corresponding to the two possible moves ``u0\_0'' and ``v0\_0'', as explained earlier. Of course, in this particular case, the second move is never actually played. We have here edited out the redundancy in \(\mathtt{TS}\), which is an artifact of how \(\mathtt{ttt.makeTTT}\) generates the grid.
238 Thus \(\mathtt{S0}\) and \(\mathtt{TS}\) are just \HOL{} equivalents of \(S_0\) and \(T\) as described in section \ref{sec:intro}. \( \mathtt{TS} \) is named as such to avoid clashing with the global \HOL{} term constant \( \mathtt{T} \).
269 \(\mathtt{st}\) is an optional argument. It is a \HOL{} tuple that explicitly describes the order in which state variables appear in the state tuple. \hc{} can automatically calculate the state from \(\mathtt{S0}\) and \(\mathtt{TS}\), but in some cases the user may wish to use the resulting theorems in other work where the state tuple has already been defined in a certain manner. \(\mathtt{st}\) is used in such cases. Note we do not use the identifier \texttt{state} as this already exists in the default HOL interactive session namespace.
299 The first property describes the initial state of the system. Note how atomic propositions are formally modelled as boolean functions on the state. As noted earlier, all atomic propositions are currently just boolean variables. \texttt{C\_BOOL} and \texttt{B\_PROP} are type constructors from the \HOL{} datatype for \ctl formulas. Property specification is considered in more detail in \S\ref{sec:prop}.
355 Each element is a triple of the form \( (term\_bdd,thm,trace) \).\footnote{A \(\textup{term\_bdd}\) is an ML value that contains a \HOL{} term together with its boolean semantics represented as a BDD (see the \texttt{HolBddLib} documentation for details).} These are the BDD semantics of the property, a theorem certifying the property holds (if it does) and a counterexample or witness trace, if one could be recovered.
434 \texttt{holCheckLib} is different from other libraries in that it does not provide tools that fit in with the usual interactive theorem proving workflow. There are no tactics, and it is unlikely (though possible) that \hc{} would be called as a decision procedure during interactive proof. The reason for this is that the models checked by model checkers are represented explicitly as state machines, whereas in \HOL{} interactive proof the underlying ``model'' is simply that of higher-order logic.  Therefore, we need to specify both models and properties explicitly.
460 The model we provide to \hc{} as the ML type \texttt{model} consists of several \HOL{} terms representing various pieces of information used by \hc{}. However, \hc{} does everything by proof, and this requires a formal \HOL{} theory of the \( \mu\)-calculus as well as of Kripke structures. Hence, the terms contained in the ML \texttt{model} type are packaged into a formal \HOL{} datatype that represents a Kripke structure and is assigned a constant name for brevity. It is this name that we see in the theorem statement in place of \texttt{M}. Indeed, a full \HOL{} definition corresponding to that name would exist in the current session's namespace, and the \HOL{} terms we supplied to the ML model would appear (perhaps abbreviated) in the right hand side of that definition.
462 As long as we are restricted to model checking, this internal formal model is not important. However, \hc{} has some experimental support for model decomposition using \HOL{} (see \S\ref{sec:decomp} for details). This requires manipulation of the formal model and then it becomes important to know what the models contain. For the moment this support is automatic, so in-depth knowledge of formal models is not required. This subsection is here, for the moment, mainly as an explanation for what we see in the \hc{} output theorems.
466 \hc{} supports model checking for \ctl and \(\mu\)-calculus properties. It is beyond the scope of this description to describe these languages in detail here (e.g., see \emph{Model Checking} by Clarke et al, MIT Press, 1999). Properties are specified as \HOL{} terms of type \texttt{ctl} or \texttt{mu}.
469 \caption{\HOL{} \(\mu\)-calculus formula syntax}
473 \(\mu\)-calculus operator & \HOL{} type constructor & Overloaded syntax \\
490 The type constructors for \texttt{mu} \index{holCheckLib!properties!mucalculus@\(\mu\)-calculus} are shown in Table \ref{tab_mu}, together with overloaded syntax for ease of entry. For example, the property saying that there exists a path to a state where \( v_0 \land v_1 \) holds is represented by the \(\mu\)-calculus formula \( \mu Q. (v_0 \land v_1) \lor \langle.\rangle Q \) and would be written in \HOL{} as
496 Note that atomic propositions are written as functions on the state, and that \(\mu\)-calculus variables and action names are modelled as \HOL{} strings. For internal reasons, these strings must be alphanumeric with underscores, and begin with a letter, the only exception being the special ``.'' action.
498 Clearly, \(\mu\)-calculus ``variables'' as modelled above are not treated as variables by \HOL{}. We use strings because \HOL{} does not have native support for variable binding in higher-order abtract syntax (this is an active research area). The treatment of free and bound variables within \hc{} is however consistent with standard definitions.
501 \caption{\HOL{} \ctl formula syntax}
505 \ctl operator & \HOL{} type constructor & Overloaded to \\
520 The example property above is the \ctl formula \( \mathbf{EF} (v_0 \land v_1) \) and would be written in \HOL{} as
534 One of the motivations behind \hc{} is to see if tight integration with \HOL{} helps the model checking work flow. In this spirit, \hc{}  includes some experimental support for model decomposition. The basic idea is that if the model consists of several components joined by parallel synchronous composition, then a property holding in one component should hold in the entire model. This seeks to exploit locality in the structure of models and properties.
566 A failure to discharge all assumptions means a completeness bug in the \hc{} proof verification machinery. However, it does not invalidate the soundness of the theorem, modulo the soundness of \HOL{}.
572 For the moment, \hc{} does not support persistence for models. The theorems produced can however be saved to permanent storage as \HOL{} theorems.

Indexes created Tue Sep 03 12:52:19 MDT 2024