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.
Cite
CITATION STYLE
Yu, Y., Manolios, P., & Lamport, L. (1999). Model checking TLA+ specifications. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1703, pp. 54–66). Springer Verlag. https://doi.org/10.1007/3-540-48153-2_6
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
