Software Modelling with TLA+

Using modelling software leads to simpler, safer systems built more quickly and cheaply
Hillel Wayne

Software Modelling with TLA+

Software Modelling with TLA+

Hillel Wayne
🇬🇧 English
Advanced

Antwerp, Belgium
Carnot Wing
Total duration: 7h00

Timezone: Europe, Amsterdam
Tuesday June 3 09:30 - 17:30


Summary

Most software flaws have one of two causes.

Sometimes the cause is that the code does not match the developer's design. Most software correctness techniques - types, tests, etc - are used to check for this issue. But other times, the code correctly implements a bad design: there is a fundamental error in the model of the system. These bugs are the most difficult to find and the most expensive to fix. Types and tests are not enough for these bugs.

The answer is software modelling. By specifying the design in a software modelling tool, developers can directly test the design for bugs without having to write any code first. Modelling software leads to simpler, safer systems built more quickly and cheaply.

One such modelling tool is TLA+. TLA+ is designed to model concurrent and distributed systems, and has successfully found bugs in everything from cloud services and message queues to video games and SSD firmware.

In this class, students will learn the basics of TLA+ from one of the foremost experts on teaching these techniques. The workshop will cover the fundamental theory of specification with several in-depth examples, and conclude with modelling a real system decided upon by the class.

For who?

This workshop targets senior software engineers.

Requirements

Participants will need a laptop with VSCode. They will be asked to install Java and the TLA+ VScode extension. Hillel will also provide a .zip file with class materials.

Hillel Wayne

About Hillel Wayne

Hillel is a formal methods consultant, the author of Learn TLA+ and Practical TLA+, and a member of the TLA+ and Alloy boards. His other work includes The Crossover Project, a collection of interviews with traditional-turned-software engineers, and Let's Prove Leftpad. In his free time, he juggles and makes chocolate. He did, in fact, bring enough for everyone.

All workshops by Hillel Wayne

Software Modelling with TLA+

Hillel Wayne
🇬🇧 English
Advanced

Antwerp, Belgium
Carnot Wing
Total duration: 7h00

Timezone: Europe, Amsterdam
Tuesday June 3 09:30 - 17:30


Also check out