Dr. Stephan Merz hielt am 14. Januar 2021 in der Ringvorlesung des Elitestudiengangs Software Engineering einen Gastvortrag über die Spezifikationssprache TLA+ und das dazugehörige Werkzeugportfolio. Er ist als Forscher am Inria in Nancy im Bereich der formalen Methoden tätig. In seinem Gastvortrag erklärte er die Modellierung verteilter Algorithmen in TLA+ sowie die unterschiedlichen Werkzeuge zur Arbeit mit TLA+ Spezifikationen.
Dr. Merz stellte zu Beginn die Spezifikationssprache TLA+ vor, die auf Arbeiten von Leslie Lamport zurückgeht. Dann erläuterte er kurz die grundlegenden Konzepte von TLA+ und zeigte, wie ein verteilter Algorithmus, den Edsger Dijkstra erfunden hatte, in TLA+ modelliert werden kann. Anschließend erklärte der Vortrag, wie Sicherheitseigenschaften des Algorithmus in TLA+ ausgedrückt werden und wie diese mit einem Beweiswerkzeug bewiesen werden können. Dr. Merz erläuterte die Architektur des TLA+ proof system und wie dieses mit der TLA+ Toolbox verbunden ist. Anschließend wurden zusammen mit den Studierenden des Elitestudiengangs „Software Engineering“ noch weitere interessante Korrektheitseigenschaften des Algorithmus diskutiert und gezeigt, wie diese mit einem interaktiven Beweiser bewiesen werden können.
Zum Abschluss fasst Dr. Merz die zentralen Eigenschaften von TLA+ zusammen und verwies auf die wichtigsten Werkzeuge, die Spezifikations- und Beweisentwickler bei der Arbeit unterstützen.
Text: Elitestudiengang „Software Engineering"