Verification of the Futurebus+ Cache Coherence protocol: A case study in model checking

Williams, K. and Esser, R.

This paper presents a case study for automatic verification using the Communicating Sequential Processes formalism. The case study concerns the Futurebus+ cache coherency standard; we develop a formal model of the protocol and perform some verification tasks upon it. In the process of doing so, we extend the previous solution by developing a formal specification of cache coherence that is suitable for the verification of both directory and snooping based cache coherence protocols.

Cite as: Williams, K. and Esser, R. (2004). Verification of the Futurebus+ Cache Coherence protocol: A case study in model checking. In Proc. Twenty-Seventh Australasian Computer Science Conference (ACSC2004), Dunedin, New Zealand. CRPIT, 26. Estivill-Castro, V., Ed. ACS. 65-71.

(from crpit.com) (local if available)