TLA+ Language
A TLA+ language is a formal specification language based on Temporal Logic of Actions.
References
2018
- (Wikipedia, 2018) ⇒ https://en.wikipedia.org/wiki/TLA+ Retrieved:2018-1-2.
- TLA+ (pronounced as tee ell a plus, ) is a formal specification language developed by Leslie Lamport. It is used to design, model, document, and verify concurrent systems. TLA+ has been described as exhaustively-testable pseudocode and blueprints for software systems; the TLA stands for "Temporal Logic of Actions."
For design and documentation, TLA+ fulfills the same purpose as informal technical specifications. However, TLA+ specifications are written in a formal language of logic and mathematics, and the precision of specifications written in this language is intended to uncover design flaws before system implementation is underway.
Since TLA+ specifications are written in a formal language, they are amenable to finite model checking. The model checker finds all possible system behaviours up to some number of execution steps, and examines them for violations of desired invariance properties such as safety and liveness. TLA+ specifications use basic set theory to define safety (bad things won't happen) and temporal logic to define liveness (good things eventually happen).
TLA+ is also used to write machine-checked proofs of correctness both for algorithms and mathematical theorems. The proofs are written in a declarative, hierarchical style independent of any single theorem prover backend. Both formal and informal structured mathematical proofs can be written in TLA+; the language is similar to LaTeX, and tools exist to translate TLA+ specifications to LaTeX documents.
TLA+ was introduced in 1999, following several decades of research into a verification method for concurrent systems. A toolchain has since developed, including an IDE and distributed model checker. The pseudocode-like language PlusCal was created in 2009; it transpiles to TLA+ and is useful for specifying sequential algorithms. TLA+2 was announced in 2014, expanding language support for proof constructs. The current TLA+ reference is The TLA+ Hyperbook by Leslie Lamport.
- TLA+ (pronounced as tee ell a plus, ) is a formal specification language developed by Leslie Lamport. It is used to design, model, document, and verify concurrent systems. TLA+ has been described as exhaustively-testable pseudocode and blueprints for software systems; the TLA stands for "Temporal Logic of Actions."
2018
- (Wikipedia, 2018) ⇒ https://en.wikipedia.org/wiki/TLA+#Language Retrieved:2018-1-2.
- TLA+ specifications are organized into modules. Modules can extend (import) other modules to use their functionality. Although the TLA+ standard is specified in typeset mathematical symbols, existing TLA+ tools use LaTeX-like symbol definitions in ASCII. TLA+ uses several terms which require definition:
- State - an assignment of values to variables
- Behaviour - a sequence of states
- Step - a pair of successive states in a behavior
- Stuttering step - a step during which variables are unchanged
- Next-state relation - a relation describing how variables can change in any step
- State function - an expression containing variables and constants that is not a next-state relation
- State predicate - a Boolean-valued state function
- “Invariant - a state predicate true in all reachable states
- Temporal formula - an expression containing statements in temporal logic
- TLA+ specifications are organized into modules. Modules can extend (import) other modules to use their functionality. Although the TLA+ standard is specified in typeset mathematical symbols, existing TLA+ tools use LaTeX-like symbol definitions in ASCII. TLA+ uses several terms which require definition:
1999
- (Yu et al., 1999) ⇒ Yuan Yu, Panagiotis Manolios, and Leslie Lamport. (1999). “Model Checking TLA + Specifications.” In: CHARME, vol. 99, pp. 54-66.
1993
- (Lamport, 1993) ⇒ Leslie Lamport. (1993). “Hybrid Systems in TLA +. ” Hybrid Systems