The TLA+ Specification Language

Stephan Merz

Abstract

The specification language TLA+ was designed by Lamport for formally describing and reasoning about distributed algorithms. It is described in Lamport's book Specifying Systems, which also gives good advice on how to make best use of TLA+ and its supporting tools. Systems are specified in TLA+ as formulas of the Temporal Logic of Actions TLA, a variant of linear-time temporal logic also introduced by Lamport. The underlying data structures are specified in (a variant of) Zermelo-Fränkel set theory, the language accepted by most mathematicians as the standard basis for formalizing mathematics. This choice is motivated by a desire for conciseness, clarity, and formality that befits a language of formal specification where executability or efficiency are not of major concern. TLA+ specifications are organized in modules that can be reused independently.

This chapter attempts to formally define the core concepts of TLA and TLA+ and to motivate some choices, in particular with respect to competing formalisms. Before doing so, an introductory overview of system specification in TLA+ is given using the example of a resource allocator. Lamport's book remains the definitive reference for the language itself and on the methodology for using TLA+. In particular, the module language of TLA+ is only introduced by example, and the rich standard mathematical library is only sketched.

© Springer-Verlag 2008

Available as: PDF

Reference

@InCollection{merz:tlabook,
  author = 	 {Stephan Merz},
  title = 	 {The Specification Language TLA\textsuperscript{+}},
  booktitle = 	 {Logics of Specification Languages},
  pages = 	 {401--451},
  publisher = {Springer},
  year = 	 2008,
  editor = 	 {Dines Bjørner and Martin C. Henson},
  series = 	 {Monographs in Theoretical Computer Science},
  address = 	 {Berlin-Heidelberg}
}