Course

Formal Methods for Specifying Systems (DAT912)

Facts

Course code DAT912

Credits (ECTS) 10

Semester tuition start Autumn, Spring

Language of instruction English

Number of semesters 1

Exam semester Autumn, Spring

Time table View course schedule

Literature Search for literature in Leganto

Introduction

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

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.

Required prerequisite knowledge

None

Exam

Project

Weight 1/1

Duration 1 Semesters

Marks Passed / Not Passed

Exam system Canvas

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.

Coursework requirements

Oral presentation

Exercises are mandatory and must be presented during the weekly meetings.

The presentation lasts a maximum of one hour.

Method 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.

Using AI to support learning and study activities

AI tools may be used in DAT912 as a learning aid, but must never substitute for the understanding of formal methods for system specification the course builds — specifying a system design formally and carrying out model checking and proofs yourself is precisely what you must master. Productive uses include asking AI to explain a concept (e.g., what a safety and liveness property is, how model checking works, or how the state space is limited), to review or debug code you have written yourself, or to suggest tests and edge cases. Any use of AI must always be disclosed in your submission as specified in the syllabus, and you remain responsible for critically evaluating whatever the AI produces.

Open for

Technology and Natural Science - PhD programme

Course assessment

The faculty decides whether early dialogue will be held in all courses or in selected groups of courses. The aim is to collect student feedback for improvements during the semester. In addition, a digital course evaluation must be conducted at least every three years to gather students’ experiences.

Contact

Course coordinator:
Hein Meling
Head of Department:
Tom Ryen
Course teacher:
Leander Nikolaus Jehl

Offered by

Faculty of Science and Technology

Department of Electrical Engineering and Computer Science

The course description is retrieved from FS (Felles studentsystem). Version 1