manolios@cc.gatech.edu
College of Computing
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)
|
Last updated October 2001 manolios@cc.gatech.edu |
College of Computing |