- TLA+ ist eine Sprache, um Software zu modellieren – auf einer höheren Ebene als dem Code – und Hardware zu modellieren – auf einer höheren Ebene als der Schaltungsebene
- Es bietet eine integrierte Entwicklungsumgebung (IDE), mit der sich Modelle schreiben und prüfen lassen
- Das von Ingenieurinnen und Ingenieuren am häufigsten verwendete Werkzeug ist der TLC-Model-Checker; außerdem gibt es einen Proof Checker
- TLA+ basiert auf Mathematik und ähnelt keiner Programmiersprache
- Für die meisten Ingenieurinnen und Ingenieure ist der Einstieg über PlusCal einfacher als direkt über TLA+
- TLA+-Modelle werden allgemein als „Spezifikation“ (Specification) bezeichnet. In der folgenden Einführung werden sie „Modelle“ genannt
PlusCal
- PlusCal ist eine Sprache zum Schreiben von Algorithmen, insbesondere von parallelen und verteilten Algorithmen
- Es wird verwendet, um Algorithmen statt als Pseudocode als präzisen, testbaren Code zu schreiben
- Es sieht wie eine einfache Programmiersprache aus und bietet Konstrukte zur Darstellung von Nebenläufigkeit und Nichtdeterminismus
- Da mathematische Formeln als Ausdrücke verwendet werden können, ist es sehr ausdrucksstark
- PlusCal-Algorithmen werden in TLA+-Modelle umgewandelt und können mit TLA+-Werkzeugen verifiziert werden
- Weil es wie eine Programmiersprache aussieht, ist es leicht zu erlernen; für die Strukturierung komplexer Modelle ist TLA+ jedoch besser geeignet
Was ist ein Modell?
- Computer und Netzwerke folgen kontinuierlichen physikalischen Gesetzen, aber ihr Verhalten lässt sich natürlicherweise als Menge diskreter Ereignisse modellieren
- Es gibt kein Modell, das ein reales System vollständig beschreibt; ein Modell beschreibt bestimmte Aspekte eines Systems für einen bestimmten Zweck
- TLA+ ist eine zustandsbasierte Modellierungssprache, die die Ausführung eines Systems als Folge von Zuständen darstellt
- Ein Ereignis wird als Paar zweier aufeinanderfolgender Zustände dargestellt; dies wird als „Schritt“ (step) bezeichnet
- Ein System wird als Menge von Aktionen modelliert, die alle möglichen Ausführungen beschreiben
Modellierung oberhalb der Code-Ebene
- TLA+ wird zur Modellierung von Systemen oberhalb der Code-Ebene verwendet
- Zum Beispiel kann der euklidische Algorithmus nicht als Code, sondern als Verfahren beschrieben werden, das den größten gemeinsamen Teiler (GCD) berechnet
- Setze die Variable x auf M und y auf N
- Subtrahiere den kleineren der Werte x und y wiederholt vom größeren Wert
- Wiederhole dies, bis x und y gleich sind; dieser Wert ist der GCD
- Eine solche Beschreibung lässt Details wie Variablentypen oder Ausnahmebehandlung aus und drückt nur das wesentliche Algorithmuskonzept aus
- Wer sich nur aufs Codieren konzentriert, findet schwer gute Algorithmen → abstraktes Denken ist nötig
- Die meisten Programmierer beginnen ohne ein High-Level-Modell mit dem Codieren, was zu Entwurfsfehlern führt
- TLA+ ist eine High-Level-Modellierungssprache, mit der sich das Verhalten und die Funktionsweise von Code klar beschreiben lassen
- Je komplexer ein System ist, desto wichtiger ist Vereinfachung; sie wird nicht durch Codierungstechnik, sondern durch höherstufiges Denken erreicht
- In einem Industrieprojekt konnte durch TLA+-Modellierung der Codeumfang eines Echtzeitbetriebssystems auf ein Zehntel reduziert werden
- Modellierung ist wirksam, um Entwurfsfehler früh zu finden, und verlässlicher als Tests oder nachträgliche Codekorrekturen
Modellierung paralleler Systeme
- Parallele Systeme bestehen aus mehreren Komponenten (Prozessen), die gleichzeitig arbeiten
- Verteilte Systeme bestehen aus räumlich getrennten Prozessen, die über Nachrichten kommunizieren
- TLA+ modelliert den Gesamtzustand des Systems als globalen Zustand
- Nach mehr als 40 Jahren Erfahrung ist die Modellierung verteilter Systeme auf Basis globaler Zustände allgemein am nützlichsten
Zustandsmaschine (State Machine)
- TLA+ definiert eine Menge von Aktionen durch die folgenden zwei Elemente:
- Anfangsbedingung: legt mögliche Startzustände fest
- Nächster-Zustand-Relation: legt mögliche Schritte fest (Paare aufeinanderfolgender Zustände)
- Die Menge der Aktionen, die diese beiden Bedingungen erfüllt, ist das Modell
- Ein solches Modell wird Zustandsmaschine (state machine) genannt
- Eine endliche Zustandsmaschine (finite-state machine) ist eine Zustandsmaschine mit endlich vielen Zuständen
- Eine Turing-Maschine ist ein Beispiel für eine Zustandsmaschine; bei einer deterministischen Turing-Maschine gibt es pro Zustand höchstens einen Folgezustand
- Eine praktische Methode, die Bedeutung einer Programmiersprache präzise zu beschreiben, ist eine operationale Semantik, die sie in eine Zustandsmaschine übersetzt
- Die Nächster-Zustand-Aktion legt nur fest, welche Schritte auftreten können; sie bedeutet nicht, dass sie auftreten müssen
- Um festzulegen, dass ein Schritt zwingend eintreten muss, muss eine Fairness-Bedingung (fairness property) hinzugefügt werden
- Auch ohne Fairness reicht es, um Ausführungsfehler zu finden, aber Auslassungsfehler werden nicht erkannt
- In den meisten Fällen gibt es mehr commission-Fehler; Einsteiger sollten daher mit dem Schreiben von Anfangsbedingungen und Nächster-Zustand-Relationen beginnen
Verifikation von Eigenschaften
- Ein Modell wird erstellt, um zu prüfen, ob ein System wie gewünscht funktioniert
- Mit TLA+-Werkzeugen lässt sich verifizieren, ob das Modell eine bestimmte Eigenschaft in allen möglichen Ausführungen erfüllt
- Beispiel: Selbst wenn die Ausführung in 99 % der Anfangszustände normal endet, muss verifiziert werden, dass alle Ausführungen normal enden
- Die häufigste Eigenschaft ist die Invarianz-Eigenschaft (invariance property), die in jedem Zustand immer wahr sein muss
- Modelle mit Fairness-Bedingungen müssen auch Lebendigkeitseigenschaften (liveness property) prüfen → z. B. dass eine Ausführung sicher terminiert
- Komplexere Eigenschaften lassen sich als Zustandsmaschine ausdrücken, und es kann verifiziert werden, ob eine andere Zustandsmaschine sie implementiert
- In TLA+ gibt es keinen formalen Unterschied zwischen Zustandsmaschine und Eigenschaft; beide werden gleichermaßen als mathematische Formel ausgedrückt
- Dass eine Zustandsmaschine eine andere implementiert, bedeutet, dass die entsprechende Formel logisch enthalten ist
- In der Praxis werden meist nur Invarianzen und einfache Lebendigkeitseigenschaften geprüft, aber auch das Verständnis komplexerer Konzepte hilft, Codefehler zu vermeiden
Die Sprache TLA+ selbst
- TLA+ ist eine mathematisch basierte Sprache und sieht nicht wie eine Programmiersprache aus
- Da Programmierer eher an Programmiersprachen als an mathematische Notation gewöhnt sind, kann es anfangs schwierig wirken
- Tatsächlich ist Mathematik jedoch ausdrucksstärker als eine Programmiersprache
- Beispiel: GCD kann als die größte positive ganze Zahl definiert werden, die zwei Zahlen teilt (ohne anzugeben, wie sie berechnet wird)
- Eine mathematische Definition kann nur das für den Zweck Wesentliche beibehalten und unnötige Implementierungsdetails abstrahieren
- Prozeduralisierung bietet keine Abstraktion, sondern versteckt Code nur an anderer Stelle
- PlusCal eignet sich gut als Einstieg in TLA+, und auch Fortgeschrittene bevorzugen PlusCal für einfache Modelle
- Wer jedoch mathematisch denken und auf hohem Abstraktionsniveau modellieren will, sollte TLA+ selbst beherrschen
3 Kommentare
https://cacm.acm.org/research/… Wird bei AWS gut eingesetzt.
Codieren ist nicht Programmieren
Weil es in diesem Artikel erwähnt wurde, habe ich danach gesucht.
Ich habe es in diesem Artikel auch zum ersten Mal gesehen und deshalb danach gesucht.