TLA+ Workshop

Der Referent

Markus Kuppe blickt auf mehr als zwanzig Jahre Erfahrung in der Softwareentwicklung zurück und ist seit über einem Jahrzehnt Mitglied des TLA+-Projekts. In dieser Zeit hat er mit Abstand die meisten Änderungen am TLA+-Tools Repository vorgenommen. In mehr als zwei Dutzend Kursen hat er umfangreiche Erfahrung im Unterrichten von Softwareentwicklern in TLA+ gesammelt und hält regelmäßig Vorträge über TLA+ in akademischen Einrichtungen und im industriellen Umfeld. Er hat zu TLA+ veröffentlicht, und seine Masterarbeit in der Informatik unter der Anleitung von Leslie Lamport mit Auszeichnung absolviert. Markus arbeitet seit acht Jahren als Principal Research Software Engineer bei Microsoft Research.

TLA+ und der Workshop

Die Entwicklung von komplexen Software-Systemen ist ein schwieriger Prozess. Obwohl die Softwareentwicklung in den Bereichen der Programmierung und des Betriebs bedeutende Fortschritte gemacht hat, stecken die Werkzeuge und Techniken für die Designphase der Entwicklung noch in den Kinderschuhen. Traditionelle Methoden wie Whiteboard-Skizzen und Design-Dokumente in Kombination mit manuellem Testen scheitern häufig daran Designfehler frühzeitig zu erkennen und zu verhindern. Dadurch entstehen teure Fehler während der Implementierung und des Betriebs, die sowohl schwer zu diagnostizieren als auch zu beheben sind.

TLA+ ermöglicht es präzise Designs von reaktiven Systemen zu erstellen und sie mit formalen Methoden zu analysieren, noch bevor die teurere Implementierungsphase beginnt. Dadurch können Fehler frühzeitig erkannt und korrigiert werden, was zu einem effizienteren und effektiveren Entwicklungsprozess führt. Das Werkzeug TLA+ macht Entwickler agiler und dessen Einsatz resultiert in einem robusteren Endprodukt.

TLA+ wird erfolgreich sowohl bei Branchengrößen wie Amazon und Microsoft als auch bei einer Vielzahl von kleineren Unternehmen eingesetzt. Wegen seiner Vielseitigkeit kommt es unter anderem bei der Entwicklung von global-verteilten Datenbanksystemen wie Cosmos DB und Speichersystemen wie S3 zum Einsatz, hilft bei der Entwicklung von Hardwarearchitekturen, oder wird zur Modellierung von Supply Chains genutzt.

‘Designing Complex Systems with TLA+’ ist ein zweitägiger Kurs, der sich auf die praktische Anwendung von TLA+ beim Design reaktiver Systeme fokussiert. Der Workshop ist für professionelle Softwareentwickler gedacht, die gewöhnlich an nebenläufigen oder verteilten Systemen arbeiten und ihr Wissen um TLA+ erweitern möchten. Im Laufe des Kurses werden die Teilnehmer TLA+ zur Modellierung eines nicht-trivialen, verteilten Systems einsetzen. Am Ende des Kurses werden die Teilnehmer ihre erste Spezifikation geschrieben und mit den TLA+ Tools ihre Korrektheit in Hinsicht auf formale Sicherheits- und Lebendigkeitseigenschaften geprüft haben. Kurzum, der Kurs bietet eine umfassende Einführung in TLA+ und beschleunigt den Weg der Teilnehmer TLA+ zu meistern.

Vorbereitung

Die detaillierte Agenda des Kurses findet sich auf
https://github.com/tlaplus-workshops/ewd998/issues/1
Darüber hinaus sind alle Workshop-Materialien unter
https://github.com/tlaplus-workshops/ewd998/
verfügbar. Um sich auf den Workshop vorzubereiten, empfehlen wir Leslie Lamports TLA+ Einführungsvideo. Um den Workshop reibungslos ablaufen zu lassen, werden wir eine browserbasierte TLA+ IDE verwenden, wofür ein GitHub-Konto benötigt wird. Vorherige Erfahrungen mit formalen Methoden oder TLA+ helfen natürlich, sind aber keine Voraussetzung.

Endorsements

“TLA+ is an indispensable tool for any engineer designing a distributed system/cloud service. At Microsoft, we have used it extensively in building services like the Cosmos DB (a globally distributed database) and Singularity (a cloud-scale AI scheduling system) and have found it extremely useful to catch design bugs upfront. Markus Kuppe is great at explaining TLA+ and its applications in designing real-world systems.” Dharma Shukla (Technical Fellow)

“TLA+ is a language with a set of tools for modeling programs and systems. It can help simplify their design and can catch bugs before any code is written. TLA+ is especially useful for building concurrent and distributed systems. Markus Kuppe understands and is very good at explaining TLA+ and how it is used in industry.” Leslie Lamport (Turing Award Winner & TLA+ creator)

Weiterführende Informationen

Use of Formal Methods at Amazon Web Services:
https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf
TLA+: Viewed from 40,000 Feet and Ground Level:
https://www.youtube.com/watch?v=Ocxczi-CvRQ
Let’s shift-shift left: How modeling can help software engineering:
https://www.youtube.com/watch?v=yJdY-RNlpuE

——————–

ENGLISH VERSION

Bio

Markus Kuppe is a seasoned TLA+ expert and a member of the TLA+ project team for over a decade, during which he became the top contributor to the TLA+ tools. Markus has spent the last eight years as a Principal Software Engineer at Microsoft Research. He has extensive experience teaching TLA+, having taught more than two dozen TLA+ classes. Markus has also published papers on TLA+ and holds a master’s degree in computer science from the University of Hamburg, which he completed with honors under the guidance of Leslie Lamport. Markus is among the world’s best TLA+ experts and has given many talks on TLA+ both in academic settings and at industry venues worldwide. He is the perfect instructor for anyone looking to learn about TLA+ and its applications in concurrent and distributed systems.

Pitch

Building large, complex software systems is hard. While software engineering has made significant strides in the areas of programming and operating systems in production, the tools and techniques available for the design stage of development have yet to mature. Traditional methods, such as whiteboard sketches and design documents combined with manual reviews, usually fail to identify and prevent design errors, leading to hard-to-detect and costly to-correct bugs downstream during the implementation and operation phases.

The TLA+ specification language offers a solution to this problem by providing a rigorous and formal method for specifying and reasoning about the behavior of complex systems, such as concurrent and distributed ones, before their actual implementation. This allows for early identification and correction of errors, leading to a more efficient and effective development process. TLA+ is also an excellent prototyping tool, making developers more agile while producing a more robust final product.

TLA+ has been successfully applied in a wide range of companies, from industry leaders like Amazon and Microsoft to smaller organizations, and across various projects, including planetary-scale storage systems, state machine replication protocols, and hardware architecture. By utilizing TLA+ in the design phase, software teams greatly improve the quality and reliability of their software systems.

Designing Complex Systems with TLA+ is a two-day, instructor-led course focusing on the practical application of TLA+ in the design of concurrent and distributed systems. This workshop is designed for professional software engineer craftsmen working on concurrent and distributed systems who want to add the TLA+ specification language and rigorous formal methods to their software engineering toolbelt.
Throughout the course, participants will learn TLA+ and how to apply it to modeling non-trivial systems in a hands-on workshop emphasizing practical application rather than just learning the language with toy examples. By the end of the workshop, participants will have written a real-world specification and checked safety and liveness properties. In short, the course provides a comprehensive introduction to TLA+ and fast-tracks participants on their path to TLA+ mastery.

Prerequisites

The detailed agenda for the course can be found at
https://github.com/tlaplus-workshops/ewd998/issues/1
Additionally, all workshop materials are available at
https://github.com/tlaplus-workshops/ewd998/
To prepare for the workshop, we recommend watching Lamport’s introductory video [1]. For the workshop to run smoothly, we will use a browser-based TLA+ IDE. Thus, Participants must have a GitHub account. Prior formal methods or TLA+ exposure obviously helps, but it is not a prerequisite.

Endorsements

Testimonies

“No competition the best training I have taken since joining Microsoft!”
“I know a few other folks [that] are signed up for later sessions. They’re in for a treat!”
“How you teach it is fantastic […]! Love the […] interactive teaching!”
“…I was amused that word of how good your workshop was already reached my friend doing formal verification at IST Austria…”

Links:

https://lamport.azurewebsites.net/tla/tla.html
Use of Formal Methods at Amazon Web Services:
https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf
TLA+: Viewed from 40,000 Feet and Ground Level:
https://www.youtube.com/watch?v=Ocxczi-CvRQ
Let’s shift-shift left: How modeling can help software engineering:
https://www.youtube.com/watch?v=yJdY-RNlpuE