Automatic checking of aggregation abstractions through state enumeration

Aggregation abstraction is a way of defining a desired correspondence betwe en an implementation of a transaction-oriented protocol and a much simpler idealized version of the same protocol. This relationship can be formally v erified to prove the correctness of the implementation. We present a technique for checking aggregation abstractions automatically using a finite-state enumerator, The abstraction relation between implement ation and specification is checked on-the-fly and the verification requires examining no more states than checking a simple invariant property. This t echnique can be used alone for verification of finite-state protocols, or a s preparation for a more general aggregation proof using a general-purpose theorem-prover. We illustrate the technique on the cache coherence protocol used in the FLASH multiprocessor system.