Automatic Checking of Aggregation Abstractions Through State Enumeration

c Checking of Aggregation Abstractions Through State Enumeration Seungjoon Park, Member, IEEE, Satyaki Das, and David L. Dill, Member, IEEE —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. nt a technique for checking aggregation abstractions cally 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.

• Type: Conference
• Year: 1997
• Where: FORTE
• Authors: Seungjoon Park, Satyaki Das, David L. Dill
• Keywords: Abstractions Through State, Aggregation Abstractions, FORTE 1997, FORTE 2007, IEEE —Aggregation Abstraction