Sciweavers

Share
FORTE
1997

Automatic Checking of Aggregation Abstractions Through State Enumeration

8 years 8 months ago
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.
Seungjoon Park, Satyaki Das, David L. Dill
Added 01 Nov 2010
Updated 01 Nov 2010
Type Conference
Year 1997
Where FORTE
Authors Seungjoon Park, Satyaki Das, David L. Dill
Comments (0)
books