INF4230 – Formal modeling and analysis of communicating systems

Schedule, syllabus and examination date

Choose semester

Course content

Use of formal methods for modeling and analyzing communicating distributed systems, with emphasis on high-level object-oriented design and programming as well as tool-based simulation/testing/prototyping and further analysis by execution. Different forms of synchronization are treated, in particular asynchronous communication through message passing. Non-trivial examples will include network communication protocols, distributed databases, and/or Internet programming.

The formalism used is based on term rewriting techniques. The course gives an introduction to the use of the language and tool Maude for the modeling and automated analysis of communicating systems, as well as to formal reasoning about properties such as termination and invariance.

Learning outcome

Show how formal methods can be used to model complex distributed systems at a high level of abstraction, so that it is possible to prototype, model check, and reason about such systems at an early stage of the system development process. The course gives a practical introduction to the design, programming, simulation/testing, and model checking of distributed systems, while also providing theoretical insight into formal reasoning about program properties.


Students who are admitted to study programmes at UiO must each semester register which courses and exams they wish to sign up for in Studentweb.

If you are not already enrolled as a student at UiO, please see our information about admission requirements and procedures.


Formal prerequisite knowledge


Recommended previous knowledge

INF1020 – Algorithms and data structures (discontinued) /INF 110.

Overlapping courses

10 credits with INF3230 – Formal modeling and analysis of communicating systems (continued), 10 credits with INF 220, 9 credits with INF 220A and 3 credits with IN 307


3 hours of lectures and 2 hours of problem sessions per week. The students must hand in and pass obligatory tasks before they are admitted to take the exam.


Midterm exam (app. 37%). Written examination at the end of the semester (app. 63%). Graded marks (A - F).


Note that the first lecture is compulsory. The subject is regarded equal to INF3230, INF220 and INF220A when practicing exam regulations.

Course Auditor: Michal Walicki

Facts about this course




Spring 2007

Spring 2006

Spring 2005

Spring 2004

This version of the course will be held for the last time Spring 2007. INF3230 – Formal modeling and analysis of communicating systems (continued) will still be held.


Every spring

Teaching language

Norwegian (English on request)