Course
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.
Dette er emnebeskrivelsen for studieåret 2025-2026
Fakta
Emnekode
DAT912
Vekting (stp)
10
Semester undervisningsstart
Autumn
Undervisningsspråk
English
Antall semestre
1
Vurderingssemester
Autumn
Content
The course covers advanced topics in formal methods for specifying systems, emphasizing languages and tools for model checking and proving the 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 a system's safety and temporal 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 specify a system design formally.
- 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.
Forkunnskapskrav
Distributed Systems (DAT520)
Discrete Mathematics (MAT120)
Exam
| Form of assessment | Weight | Duration | Marks | Aid |
|---|---|---|---|---|
| Project | 1/1 | 1 Semesters | Passed / Not Passed |
A final group project must 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.
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 may receive a different result based on their performance during the oral examination.
Vilkår for å gå opp til eksamen/vurdering
Exercises are mandatory and must be presented during the weekly meetings.
The presentation lasts a maximum of one hour.
Fagperson(er)
Course coordinator:
Hein MelingHead of Department:
Tom RyenCourse teacher:
Leander Nikolaus JehlMethod of work
We meet weekly for 4 hours and discuss selected exercises from the course material. Each student walks through their solution. Later in the course, the group will specify a selected system and prove its safety and liveness properties.
The course is only given on demand. The working method may deviate in the case of meager student numbers.
