Presented at
May Contain Hackers (MCH2022),
July 24, 2022, 4 p.m.
(180 minutes).
[TLA+, the temporal logic of actions](https://en.wikipedia.org/wiki/TLA+), is a high-level specification language to design, document, and verify reactive systems. It has been around for two decades and is used in [academia](https://hal.inria.fr/hal-00768812) and by [hardware-](https://lamport.azurewebsites.net/tla/intel-excerpt.html?back-link=industrial-use.html?unhideBut@EQhide-intel@AMPunhideDiv@EQintel), and [software-people](https://probablydance.com/2020/10/31/using-tla-in-the-real-world-to-understand-a-glibc-bug/) [at](https://www.youtube.com/watch?v=x9zSynTfLDE) [various](https://www.elastic.co/elasticon/conf/2018/sf/reliable-by-design-applying-formal-methods-to-distributed-systems) companies. Its application spans the design of [complex cloud systems](https://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/fulltext), [concurrent and distributed](https://github.com/tlaplus/Examples/tree/master/specifications/PaxosHowToWinATuringAward) algorithms, processor hardware vulnerabilities [(spectre/meltdown)](https://www.youtube.com/watch?v=Le1R9P5H9C4), ...
TLA+ has been described as a lightweight formal method, debuggable design, and the missing link between code and design documents.
This workshop shows how to design a distributed system in TLA+, focusing on applying TLA+ rather than the language's theory. More specifically, we cover parts of my [tutorial](https://github.com/tlaplus-workshops/ewd998) on modeling a [termination detection algorithm](https://www.cs.utexas.edu/users/EWD/ewd09xx/EWD998.PDF). This is a hands-on, interactive workshop. Come and find out what modeling and TLA+ are good for.
Presenters:
-
Markus Kuppe
I have been a member of the TLA+ project for over a decade, and I have the privilege to contribute to TLA+ as part of my [day job](https://github.com/lemmy/). Besides working on its tools, I've been running the workshop/class on multiple occasions. Before getting involved with TLA+, I thought formal methods wouldn't be useful in practice, but first-hand experience convinced me otherwise.
I tweet at [@lemmster](https://twitter.com/lemmster).
Links:
Similar Presentations: