Checking Cache Coherence Protocols with TLA+
Rajeev Joshi, Leslie Lamport, John Matthews, Serdar Tasiran, Mark Tuttle, and Yuan Yu
March 2003
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.
 PDF file |  PostScript file |
In: Journal of Formal Methods in System Design
Publisher: Kluwer Academic
All copyrights reserved by Kluwer Academic 2003.
Details
| Type: | Article |
| URL: | http://www.wkap.nl/kaphtml.htm/ |
| Pages: | 125-131 |
| Volume: | 22 |
| Number: | 2 |
©2009 Microsoft Corporation. All rights reserved.