Verification via Model Checking

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

Symbolic Model Checking reference.

Your Assignment

Reference

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

The software source

Algorithm Details

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.

CTL formula subdivision

An input formula to be checked must be broken down into sub-formulae until you get to the atomic formula level. Once you have atomic formulae you can directly check them in each state against the list of atomic formulae in the model. Consider the above example:

  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

marking the states of the model

For any particluar formula P to be checked, we traverse the state graph of the model and mark on each state if the formula is T or F in that state. When the entire model has been traversed, we are left with P being added to each state formula list just like the atomic forumulae are. So for any state Si we can, by examination, determine the truth of

  Si  |= P

For most situations, we are interested is seeing if P is true in S0 the initial state of the computation.

bottom-up handling of each sub-forumla

Once the formula is subdivided, you start at the bottom of the tree and begin to check the truth of each sub-formula in the structure (model). Each state in the model is marked as having the subformula either T or F in that state (just as the atomic formulae are). You do this by writing a function to handle each operator in the CTL language.

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.

delivery of response

Our final objective is to report whether nf[1] is T or F in state s0.