Generate & Check Method for Verifying Transition Systems in CafeOBJ 

An interactive theorem proving method for the verification of infinite state transition systems is described.

The state space of a transition system is defined as a quotient set (i.e. a set of equivalence classes) of terms of a topmost 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.