|
1. |
Automatic checking of aggregation abstractions through state enumeration
Seungjoon Park; Das, S.; Dill, D.L.;
Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
Volume 19,
Issue 10,
Oct. 2000
Page(s):1202
-
1210
Abstract:
Aggregation abstraction is a way of defining a desired correspondence between an implementation of a transaction-oriented protocol and a much simpler idealized version of the same protocol. This relationship can be formally verified 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 implementation and specification is checked on-the fly and the verification requires examining no more states than checking a simple invariant property. This technique can be used alone for verification of finite-state protocols, or as 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
|
Cart
