en_GB
Hold Ctrl-tasten nede. Trykk på + for å forstørre eller - for å forminske.

DAT912_1

Formal Methods for Specifying Systems

This is the study programme for 2019/2020. It is subject to change.


The course covers advanced topics in formal methods for specifying system designs, model checking and proving safety and liveness properties.

Learning outcome

Knowledge
  • 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.

Skills
  • 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.

General competency
  • Know how to specify and prove or model check properties of advanced distributed computer systems.

Contents

The course covers advanced topics in formal methods for specifying systems, with particular emphasis on tools for model checking and proving safety and liveness properties of system designs and specifications.
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

DAT520 Distributed Systems, MAT120 Discrete Mathematics
DAT520 Distributed Systems, MAT120 Discrete Mathematics

Recommended previous knowledge

DAT530 Discrete Simulation and Performance Analysis, DAT600 Algorithm Theory
DAT600 Algorithm Theory, DAT530 Discrete Simulation and Performance Analysis 

Exam

Weight Duration Marks Aid
Report1/1 Pass - Fail
The group project report will be evaluated with pass/fail. All group members must contribute equally to all aspects of the report and development of TLA+ specifications, models etc. Each group member can receive a different result based on their performance during an oral examination.

Coursework requirements

TLA+ exercises are mandatory and must be presented during the weekly meetings.
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.

Course teacher(s)

Course teacher
Leander Nikolaus Jehl
Course coordinator
Hein Meling

Method of work

We meet weekly for 4 hours and discuss selected exercises from the course material. Each student walks through his/her solution. Later in the course, the group will specify a selected system and prove liveness and safety properties for the system in question.

Literature

  • Selected chapters from the TLA+ Hyperbook.
  • Selected chapters from the Specifying Systems book.
  • Video lectures by Leslie Lamport


This is the study programme for 2019/2020. It is subject to change.

Sist oppdatert: 13.11.2019

History