Generate & Check Method in CafeOBJ Revised

• Kokichi Futatsugi

A new method for verification of transition systems is presented.

The state space of a transition system is defined as a quotient set (i.e. a set of equivalence classes) of terms of a top most sort State, and the transitions are defined with conditional rewrite rules over the quotient set. A property to be verified is either (1) an invariant (i.e. a state predicate that is valid for all reachable states) or (2) a (p leads-to q) property for two state predicates p and q. Where (p leads-to q) means that from any reachable state s with (p(s) = true) the system will get into a state t with (q(t) = true) no matter what transition sequence is taken.

Verification is achieved by developing proof scores in CafeOBJ. Sufficient verification conditions are formalized for verifying invariants and (p leads-to q) properties. For each verification condition, a proof score is constructed to (1) generate a finite set of state patterns that covers all possible infinite states and (2) check validity of the verification condition for all the covering state patterns by reductions.

The method achieves significant automation of proof score developments.