This is an introduction to the Temporal Logic of Actions (TLA+), the system for specifying concurrent systems invented by Turing Award winner Leslie Lamport.
In this session I will demonstrate the use of TLA+ and TLC (the TLA+ model checker) to develop a specification for, and explore the properties of, a concurrent system.
I will show how an interactive test driven approach can be used both to learn TLA+, and to incrementally build a specification for a concurrent system.
You will see how the development of a specification can be guided in simple steps by tests, whilst the TLA+ tools expose flaws that violate requirements or cause the system to deadlock.
TLA+ and the TLA+ Tools, including TLC, are available from Microsoft Research under an MIT license.