Course syllabus - Formal verification of reactive systems 7.5 credits

Formell verifiering av reaktiva system

Course code: DVA457
Valid from: Autumn semester17
Level of education: Second cycle
Subject: Informatics/Computer and Systems Scie...
Main Field(s) of Study: Computer Science,
In-Depth Level: A1N (Second cycle, has only first-cycle course/s as entry requirements),
School: IDT
Ratification date: 2017-01-31


Software verification and validation focus on detecting possible bugs in the software prior to its implementation, which is crucial to industry.  The aim of the course is to introduce the students into methods and tools for verifying systems that need to react to external stimuli. The methods use system models with precise formal semantics and will span contract-based verification, model-checking as well as deductive verification. Students will learn some of the theories of formal verification, and how to use tool support in order to verify system models as well as programs.

Learning outcomes

After completing the course, the student shall be able to:

1.  describe how formal modelling languages can be applied to model systems
2.  model discrete and real-time systems using finite state automata and timed automata
3.  specify simple system requirements in temporal logics
4.  describe the principles used to verify models in model-checking and deductive verification
5.  describe the principles of contract-based verification of programs
6.  apply tools to model and verify discrete systems and real-time systems
7.  apply contract-based tools to verify software programs (e.g., in C)

Course content

The course will cover the following topics: transition systems, modal logics, modeling, verification by model-checking, deductive formal verification, and contract-based verification of programs. Examples of tools that will be used in the course are: UPPAAL, PVS, VCC, Dafny etc.

Teaching methods

Lectures (web-based).

Specific entry requirements

120 credits, of which 80 hp in engineering or informatics, including at least 30 credits in computer science or software development.
In addition, at least 18 months of documented work experience in software development or related areas. In addition, Swedish course B/Swedish course 3 and English course A/English course 6 are required. For courses given entirely in English exemption is made from the requirement in Swedish course B/Swedish course 3.


Written assignment (INL1), 2,5 credits, (examines the learning objectives 1 and 2), Marks Fail (U) or Pass(G)
Written assignment (INL2), 2,5 credits, (examines the learning objectives 3, 4, and 6), Marks Fail (U) or Pass(G)
Written assignment (INL3), 2,5 credits, (examines the learning objectives 5 and 7), Marks Fail (U) or Pass(G)

Rules and regulations for examinations


Two-grade scale

Transitional provisions

The course overlaps with 2,5 credits towards the course Advanced Validation and Verification 7,5 credits.

Course literature is not yet public.