Checking Cache Coherence Protocols with TLA+

We have a great deal of experience using the speci¯cation language TLA+ and its model checker TLC to analyze protocols designed at Digital and Compaq (both now part of HP). The tools and techniques we have developed apply equally well to software and hardware designs. In this paper, we describe our experience using TLA+ and TLC to verify cache-coherence protocols.

fmsd.pdf
PDF file
fmsd.ps
PostScript file

In  Journal of Formal Methods in System Design

Publisher  Kluwer Academic
All copyrights reserved by Kluwer Academic 2003.

Details

TypeArticle
URLhttp://www.wkap.nl/kaphtml.htm/
Pages125-131
Volume22
Number2
> Publications > Checking Cache Coherence Protocols with TLA+