- Be familiar with the general principles of formal methods for specifying systems.
- Be familiar with the mathematics and formalism needed to formally specify a system design.
- Be familiar with techniques required to limit the state-space explosion problem.
- Be familiar with techniques for specifying safety and liveness properties and how to prove a system design adheres to the given properties using a model checker and proof system.
- Be able to develop advanced distributed system designs with fault tolerance properties.
- Be able to modularize and refine system specifications.
- Be able to machine check and prove interesting properties of a system's design.
- Know how to specify and prove or model check properties of advanced distributed computer systems.
The course is based on the Temporal Logic of Actions, or TLA+, and PlusCal languages for specifying systems. We introduce these languages with basic examples before we move on to our main target: advanced distributed system protocols such as voting, distributed transaction commit, distributed consensus (Paxos), state machine replication, and Byzantine fault tolerant protocols. We apply the TLC model checker and the TLA Proof System to verify both safety and temporal properties of systems.
The course also includes a group project in which you specify and verify liveness and safety properties of a suitable distributed system design.
Required prerequisite knowledge
Recommended previous knowledge
DAT600 Algorithm Theory, DAT530 Discrete Simulation and Performance Analysis
|Report||1/1||Pass - Fail|
A final group project is also to be completed based on a specific system design that will be decided jointly with the students. The project should be completed in TLA+ and PlusCal, and corresponding model checking and proof system results should be documented in a final report. The TLA+ files and dependencies should be submitted both separately and as part of the report, e.g. as an appendix.
Method of work
- Selected chapters from the TLA+ Hyperbook.
- Selected chapters from the Specifying Systems book.
- Video lectures by Leslie Lamport
Sist oppdatert: 11.12.2019