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.
(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 (AU (NOT X) (OR Y Z)) sf (2 4) nf (NOT X) sf (3) nf X sf nil nf (OR Y Z) sf (5 6) nf Y sf nil nf Z sf 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 and nf 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. Invoke the OR-operator function to check the truth of nf in each state as you traverse the model. This is not a temporal operator and we know how to figure the truth of nf if we know the truth of nf and nf in a state. We then mark nf 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 after all states in the model have been marked T or F for all nf through nf. We invoke the AU-operator function now to determine T or F for nf in each state.