Model checking is a general term for a collection of related formal methods. Specification of program behavior is done in a modified predicate calculus called

The techniques are applicable to all programs, but are especially useful for concurrent computations.

Symbolic Model Checking reference.

This information shows the basic model structure used by Clark's early model check "mcb".

To run this model check and try some assertions, log onto uncle-leo.cs.unc.edu (which one of our few remaining sparc machines). Here are the models, the checker, and instructions.

- Automatic Verification of Finite State Concurrent Systems using Temporal Logic , Clarke, Emperson, Sistla; ACM TOPLAS, vol. 8 (2), April 1986, pp. 244-263.

- input parsing The project will be complete if it works with "well structured" , or nested prefix, input like this:

(AU (NOT X) (OR Y Z))for example. This will allow you to concentrate on developing the ML structures and algorithms for model checking and ignore the details of text parsing more.

I will give extra credit if you provide an input parser that allows text input like that of mcb:

A [ ~x U ( y | z) ]for example. Note that to help the parser, Clarke's mcb uses the "[ ]" brackets to signal the binary UNTIL operator, and "( )" brackets to signal the unary operators.

If you have a working program for structured input, then it will be easy to go back and write an input parser to deal with converting the text into the structured ML.

A [ ~X U ( Y | Z ) ] (AU (NOT X) (OR Y Z)) nf[1] (AU (NOT X) (OR Y Z)) sf[1] (2 4) nf[2] (NOT X) sf[2] (3) nf[3] X sf[3] nil nf[4] (OR Y Z) sf[4] (5 6) nf[5] Y sf[5] nil nf[6] Z sf[6] nil

Si |= PFor most situations, we are interested is seeing if P is true in S0 the initial state of the computation.

In the example above, the nf[5] and nf[6] are atomic formulae and are checked directly against the list of atomic formula for the state being examined as you traverse the model.

Going up the tree, consider nf[4]. Invoke the OR-operator function to check the truth of nf[4] in each state as you traverse the model. This is not a temporal operator and we know how to figure the truth of nf[4] if we know the truth of nf[5] and nf[6] in a state. We then mark nf[4] as T or F in that state and keep traversing the model until all states are handled.

Keep going up the subformulae tree. We finally get to nf[1] after all states in the model have been marked T or F for all nf[2] through nf[6]. We invoke the AU-operator function now to determine T or F for nf[1] in each state.