Softwarekonferenz für parallele
und hochperformante Programmierung
Heidelberg, Print Media Academy, 19.–22. Februar 2019

// Mit TLA+ zum korrekten Parallel-Programm

Parallele Programmierung ist ein zentraler Baustein, um immer leistungsfähigere Software zu entwickeln. Diese Leistungsfähigkeit geht allerdings mit gesteigerter Komplexität einher, wodurch etablierte Werkzeuge zur Sicherstellung von Korrektheit an ihre Grenzen stoßen.

Selbst eine überdurchschnittlich hohe Test-Coverage deckt nicht im Ansatz den gesamten Zustandsraum von parallelen (und verteilten) Programmen ab. Dabei verstecken sich die besonders widerspenstigen Bugs in den "dunklen Ecken" des Zustandsraums.

In diesem Workshop wird den Teilnehmern die Möglichkeit geboten, das notwendige Wissen für den erfolgreichen Einsatz von TLA+ selbst zu erlernen, um zukünftig Licht in alle Ecken des Zustandsraums zu bringen.

Vorkenntnisse
* Es sind keine Vorkenntnisse mit formalen Methoden in Allgemeinen oder TLA+ im Besonderen nötig.
* Der Workshop richtet sich an Entwickler, die bisher nicht mit TLA+ in Berührung gekommen sind.

Lernziele
Ziel dieses Workshops ist es, den Zuhörern die Möglichkeiten formaler Methoden wie TLA+ näher zu bringen und ihnen die entscheidenden Grundlagen zu vermitteln. Der Fokus liegt dabei auf dem praktischen Einsatz von TLA+. Der akademische Unterbau wird nur am Rande behandelt.

Am Ende des Workshops sind die Teilnehmer in der Lage, Probleme mit einer TLA+ oder PlusCal-Spezifikation abzubilden, Sicherheits- und Lebendigkeitsanforderungen zu formulieren und mit Hilfe des TLC Model Checker zu prüfen.

Es werden Konzepte wie State Machines, Non-determinism, Invariants, Temporal Properties, Behaviors und Model Checking betrachtet. Weiterführende Konzepte wie Refinement Mappings oder Beweisführung mit TLAPS liegen hingegen nicht im Rahmen dieses Einführungs-Workshops.


// Markus Kuppe Markus Kuppe

beschäftigt sich mit nebenläufiger und verteilter Programmierung, um diese handhabbarer zu machen. TLA+ ist dabei sowohl Mittel als auch Zweck. Markus ist bei Microsoft Research als Principal Engineer hauptverantwortlich für den TLA+ Model Checker zuständig.