Learning Path 7: Verification of Distributed Programs with TLA+

Slides

For your convenience, the slides contain - a short summary of typical TLA+ language constructs and - an teaser on linear temporal logic

These parts are reference material and is not covered in any video.

7.0 Motivation

7.1 Introduction to TLA+ by Leslie Lamport

Chris Newcombe et al.: How Amazon Web Services Uses Formal Methods. Communications of the ACM, April 2015, Vol. 58 No. 4, Pages 66-73

Optional: Mathematical foundations

If you want to brush up your math as used in TLA+, check selected chapters of the TLA+ book

  • Chapter 1: Propositional logic, Set theory, Predicate logic
  • Chapter 8.1: Temporal logic

7.2 Example 1-Bit Clock

7.3 Safety, Liveness and Fairness

Exercise 7

(Recommended) Deadline: 09 June

Exercise 7

How to install the TLA+ Toolbox

Broadcast Specification

Reference material on TLA+