TLA+ (Temporal Logic of Actions) ist eine formale Spezifikationssprache von Leslie Lamport für nebenläufige und verteilte Systeme. Ein System wird als Menge von Zuständen und Aktionen beschrieben; die temporale Logik erfasst, welche Verhaltensabläufe möglich sind. Lamport entwickelte TLA+ in den frühen 1990er-Jahren und dokumentierte es im Buch „Specifying Systems" (Addison-Wesley, 2002).
Grundmuster einer Spezifikation
---- MODULE Counter ----
EXTENDS Naturals
VARIABLE x
Init == x = 0
Next == x' = x + 1
Spec == Init / [][Next]_x
====Ein Apostroph (x') bezeichnet den Wert der Variablen im nächsten Zustand. [][Next]_x erlaubt Stuttering-Schritte, bei denen sich nichts ändert — wichtig für die Komposition von Systemen.
Operatoren
- Logik:
/(und),/(oder),~(nicht),⇒(impliziert),A(für alle),E(es existiert). - Temporal:
[]P(immer P — Sicherheit),<>P(schließlich P — Lebendigkeit),P ~> Q(P führt zu Q),WF_/SF_(schwache/starke Fairness). - System:
ENABLED A,UNCHANGED x,[A]_v(Aktion mit Stuttering).
Sicherheit, Lebendigkeit, Verfeinerung
Eine Invariante []Inv drückt eine Sicherheitseigenschaft aus; Lebendigkeitseigenschaften sagen, dass etwas irgendwann eintritt. Mit Verfeinerungs-Abbildungen (Refinement Mappings) zeigt man, dass eine Implementierung eine abstrakte Spezifikation korrekt umsetzt.
Werkzeuge
- TLC, der Model Checker, durchsucht endliche Modelle systematisch nach verletzten Invarianten und Deadlocks.
- TLAPS, das TLA+ Proof System, beweist Eigenschaften maschinengeprüft wie ein Proof Assistant — verwandt mit Isabelle.
- PlusCal (2009) ist eine algorithmenähnliche Sprache, die zu TLA+ kompiliert.
- Die Toolbox ist die integrierte Entwicklungsumgebung mit Editor, TLC und TLAPS.
TLA+ wird unter anderem bei Amazon Web Services zur Verifikation kritischer Systemkomponenten eingesetzt. Während TLA+ zeitliches Verhalten modelliert, beschreiben Promela mit dem Model Checker SPIN ausführbare Prozessmodelle und Alloy statische Strukturen relational; Zustand und Operationen mengentheoretisch beschreibt die Z-Notation.