Panagiotis (Pete) Manolios
College of Computer and Information Science
Northeastern University

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.


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)