Elitenetzwerk: Detail
Zurück zur Übersicht

Gastvortrag von Dr. Stephan Merz

Dr. Stephan Merz hielt am 14. Ja­nuar 2021 in der Ringvorle­sung des Elite­studi­engangs Software Engi­neering ei­nen Gastvor­trag über die Spe­zi­fi­ka­ti­onsspra­che TLA+ und das dazugehö­ri­ge Wer­kzeugportfo­lio. Er ist als Forscher am In­ria in Nancy im Bereich der formalen Methoden tä­tig. In seinem Gastvor­trag er­klärte er die Model­lierung verteilter Algo­rithmen in TLA+ sowie die un­terschiedli­chen Wer­kzeuge zur Arbeit mit TLA+ Spe­zi­fi­ka­tionen.

TLA+ einsetzen

Dr. Merz stellte zu Beginn die Spe­zi­fi­ka­ti­onsspra­che TLA+ vor, die auf Arbeiten von Leslie Lamport zu­rückgeht. Dann er­läuterte er kurz die grundlegenden Konzep­te von TLA+ und zeigte, wie ein verteilter Algo­rithmus, den Edsger Dijkstra er­funden hatte, in TLA+ model­liert werden kann. Anschließend er­klärte der Vortrag, wie Si­cher­heitsei­genschaften des Algo­rithmus in TLA+ ausgedrückt werden und wie diese mit ei­nem Beweiswerkzeug bewiesen werden können. Dr. Merz er­läuterte die Architektur des TLA+ proof system und wie dieses mit der TLA+ Tool­box verbunden ist. Anschließend wurden zu­sammen mit den Studierenden des Elite­studi­engangs „Software Engineering“ noch wei­te­re in­te­ressante Korrektheitseigenschaften des Algo­rithmus disku­tiert und gezeigt, wie diese mit ei­nem in­terak­tiven Bewei­ser bewiesen werden können.
Zum Abschluss fasst Dr. Merz die zentralen Eigenschaften von TLA+ zu­sammen und verwies auf die wichtigsten Wer­kzeuge, die Spe­zi­fi­ka­tions- und Beweis­entwickler bei der Arbeit un­terstützen.

Text: Elite­studi­engang „Software Engi­neering“

n mit den Studierenden des Elite­studi­engangs