Model Checking TLA+ Specifications
Yuan Yu, Panagiotis Manolios, and Leslie Lamport.
In L. Pierre and T. Kropf, editors, Correct Hardware Design and Verification Methods, CHARME '99,
volume 1703 of LNCS, pages 54-66. Springer-Verlag, 1999.
Abstract
TLA+ is a specification language for concurrent and reactive
systems that combines the temporal logic TLA with full first-order
logic and ZF set theory. TLC is a new model checker for debugging a
TLA+ specification by checking invariance properties of a
finite-state model of the specification. It accepts a subclass of
TLA+ specifications that should include most descriptions of real
system designs. It has been used by engineers to find errors in the
cache coherence protocol for a new Compaq multiprocessor. We
describe TLA+ specifications and their TLC models, how TLC works,
and our experience using it.
Gzipped Postscript (67K)