Software Modeling with TLA+

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.