2022-07-24, 19:00–22:00, Gear ⚙️
TLA+, the temporal logic of actions, 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 and by hardware-, and software-people at various companies. Its application spans the design of complex cloud systems, concurrent and distributed algorithms, processor hardware vulnerabilities (spectre/meltdown), ...
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 on modeling a termination detection algorithm. This is a hands-on, interactive workshop. Come and find out what modeling and TLA+ are good for.
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. 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.