Verification of a multiprocessor cache protocol using simulation relations and higher-order logic

We present a formal verification method for concurrent systems. The technique is to show a correspondence between state machines representing an implementation and specification behavior. The correspondence is called asimulation relation, and is particularly well suited for theorem provers. Since the method does not rely on enumerating all the states, it can be applied to systems with an infinite or unknown number of states. The method is illustrated by proving the correctness of a particularly subtle example that is likely to be of increasing importance: a directory based multiprocessor cache protocol. The proof is carried out using the HOL (higher-order logic) theorem prover.