Checking cache-coherence protocols with TLA+

被引：31

作者：

Joshi, R

Lamport, L

Matthews, J

Tasiran, S

Tuttle, M

Yu, Y

机构：

[1] HP Labs, Syst Res Ctr, Palo Alto, CA USA

[2] Microsoft Res, Mountain View, CA USA

[3] Oregon Grad Inst, Portland, OR USA

[4] HP Labs, Cambridge Res Lab, Cambridge, MA USA

来源：

FORMAL METHODS IN SYSTEM DESIGN | 2003年 / 22卷 / 02期

关键词：

TLA(+); TLC; model checking; cache coherence;

D O I：

10.1023/A:1022969405325

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We have a great deal of experience using the specification 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.

引用

页码：125 / 131

页数：7