CTL model checker (CSP)
From LiteratePrograms
This article describes a simple Computational Tree Logic (CTL) model checker, written in the machine-readable version of CSP and intended to be evaluated using the Formal Systems Europe Ltd. FDR tool. See Huth and Ryan, "Logic in Computer Science" for details of the algorithm.
Note that this model-checker does not apply CTL formulas to CSP processes! It is a hack that tricks FDR into performing CTL model-checking of a user-defined finite state machine expressed as several different sets (not a labelled transition system, or a CSP process expression).
Contents |
Inputs
The model-checker takes as input a finite state machine expressed as sets of states, possible transitions between, and labels consisting of atomic propositions that are true in each state. For example, the finite state machine shown in the figure to the right can be represented as the sets:
<<inputs>>= const_MaxState = 10 datatype STATE = S.{0..const_MaxState} -- A set of states States = { S.0, S.1, S.2, S.3 } -- A set of transitions Trans = { (S.0, S.2), (S.0, S.3), (S.1, S.0), (S.2, S.3), (S.3, S.0), (S.3, S.1) } -- A labeling function Labels = { (S.0, {Atom.A, Atom.C}), (S.1, {Atom.C}), (S.2, {Atom.A, Atom.B}), (S.3, {Atom.B}) }
CTL formulas are expressed using a datatype that provides an abstract syntax for combining atomic propositions using various logical and temporal operators:
<<ctl syntax>>= datatype ATOM = A | B | C | D datatype CTL_FORMULA = Top | Bottom | Atom.ATOM | Not.CTL_FORMULA | And.(CTL_FORMULA, CTL_FORMULA) | Or.(CTL_FORMULA, CTL_FORMULA) | Implic.(CTL_FORMULA, CTL_FORMULA) | AX.CTL_FORMULA | EX.CTL_FORMULA | AU.(CTL_FORMULA, CTL_FORMULA) | EU.(CTL_FORMULA, CTL_FORMULA) | EF.CTL_FORMULA | EG.CTL_FORMULA | AF.CTL_FORMULA | AG.CTL_FORMULA
Here are a few examples of CTL formulas expressed using the syntax defined above:
<<example ctl formulas>>= Spec1 = EX.Atom.B Spec2 = EU.(And.(Atom.A, Atom.B), Atom.C) Spec3 = AF.Not.Atom.C Spec4 = EX.Atom.C Spec5 = AU.(Atom.C, And.(Atom.A, Atom.B))
Refinement assertions
FDR requires some kind of assertion about a process to be made in order to trigger the evaluation of a function. In the case of this script, evaluation of the model-checking function is triggered by performing a trace refinement (i.e language containment) check to see if the distinguished initial state (S.0 by convention) is a member of the set of states returned by the model-checking function. If the initial state is in the returned set of states then the model satisifes the spec, and the corresponding FDR assertion will succeed.
<<example refinement checks>>= channel state: STATE SAT_States1 = SAT(Spec1) assert state?s:SAT_States1 -> STOP [T= state!S.0 -> STOP SAT_States2 = SAT(Spec2) assert state?s:SAT_States2 -> STOP [T= state!S.0 -> STOP SAT_States3 = SAT(Spec3) assert state?s:SAT_States3 -> STOP [T= state!S.0 -> STOP SAT_States4 = SAT(Spec4) assert not state?s:SAT_States4 -> STOP [T= state!S.0 -> STOP SAT_States5 = SAT(Spec5) assert not state?s:SAT_States5 -> STOP [T= state!S.0 -> STOP
Implementation
The core of the model-checker is a boolean satisfaction algorithm that examines a CTL formula, and returns the set of states in the input finite state machine that satisfy the formula. We define the SAT function using a recursive pattern-match on the syntax of CTL formulas. The return value of the function is a set containing the states which satisfy the given CTL formula.
<<SAT>>= SAT(Top) = States SAT(Bottom) = {} SAT(Atom.p) = { s | (s, L) <- Labels, member(Atom.p, L) } SAT(Not.p) = diff(States, SAT(p)) SAT(And.(p, q)) = inter(SAT(p), SAT(q)) SAT(Or.(p, q)) = union(SAT(p), SAT(q)) SAT(Implic.(p, q)) = SAT(Or.(Not.p, q)) SAT(AX.p) = SAT(Not.EX.Not.p) SAT(EX.p) = SAT_EX(p) SAT(AU.(p, q)) = SAT(Not.Or.(EU.(Not.p, And.(Not.p, Not.q)), EG.Not.q)) SAT(EU.(p, q)) = SAT_EU(p, q) SAT(EF.p) = SAT(EU.(Top, p)) SAT(EG.p) = SAT(Not.AF.Not.p) SAT(AF.p) = SAT_AF(p) SAT(AG.p) = SAT(Not.EF.Not.p)
Temporal operators
The definitions of the SAT function for the temporal operators EX, EU, and AF are a little more complex than those required for the other operators:
<<temporal operators>>= SAT_EX(p) = let X = SAT(p) within pre_E(X) SAT_AF(p) = let Y = SAT(p) f(X) = union(X, pre_A(X)) within if Y == States then Y else Fixpoint(f, Y) SAT_EU(p,q) = let W = SAT(p) Y = SAT(q) f(X) = union(X, inter(W, pre_E(X))) within if Y == States then Y else Fixpoint(f, Y)
Auxiliary functions
The SAT_EX, SAT_AF and SAT_EU functions rely on three auxiliary functions. The first computes a "preimage" consisting of the set of all states that can transition to any state in the set X.
<<preimage E>>= pre_E(X) = { s0 | (s0, s1) <- Trans, member(s1, X) }
The second auxiliary function computes a "preimage" consisting of the set of all states which transition to states in X, and do not transition to any state outside of X. This is easily expressed in terms of set differences and the pre_E
function.
<<preimage A>>= pre_A(X) = diff( pre_E(X), pre_E( diff(States, X) ) )
The third auxiliary function computes a fixpoint for the application of a function from sets of states to sets of states.
<<fixpoint>>= Fixpoint(f, X) = let X' = f(X) within if X == X' then X else Fixpoint(f, X')
Complete script
The complete CSP script combines the inputs, refinement checks, datatypes, and SAT functions into a single file, suitable for loading into FDR.
<<ctl_model_checker.csp>>= inputs example ctl formulas example refinement checks ctl syntax SAT temporal operators preimage E preimage A fixpoint
Download code |