Formal Methods for Specifying Systems (DAT912)

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


Course description for study year 2023-2024. Please note that changes may occur.

Facts

Course code

DAT912

Version

1

Credits (ECTS)

10

Semester tution start

Spring, Autumn

Number of semesters

1

Exam semester

Spring, Autumn

Language of instruction

English

Offered by

Content

The course covers advanced topics in formal methods for specifying systems, with particular emphasis on languages and tools for model checking and proving safety, liveness and temporal properties of system designs and specifications.

We introduce these formal methods 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 a model checker and a proof system to verify both safety and temporal properties of systems.

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.

Required prerequisite knowledge

DAT520 Distributed Systems, MAT120 Discrete Mathematics

Recommended prerequisites

DAT530 Discrete Simulation and Performance Analysis, DAT600 Algorithm Theory

Exam

Form of assessment Weight Duration Marks Aid
Report 1/1 Passed / Not Passed

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 specifications, models etc. Each group member can receive a different result based on their performance during an oral examination.

Coursework requirements

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 the chosen modeling language and tool, and corresponding model checking and proof system results should be documented in a final report. The model source files and dependencies should be submitted separately and as part of the report, e.g., as an appendix.

Course teacher(s)

Course teacher:

Leander Nikolaus Jehl

Course coordinator:

Hein Meling

Head of Department:

Tom Ryen

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 the liveness and safety properties of the system in question.

The course is only given on demand. The working method may deviate in case of very low student numbers.

Course assessment

There must be an early dialogue between the course coordinator, the student representative and the students. The purpose is feedback from the students for changes and adjustments in the course for the current semester.In addition, a digital course evaluation must be carried out at least every three years. Its purpose is to gather the students experiences with the course.

Literature

The syllabus can be found in Leganto