INF4231 – Formal Modelling and Analysis of Communicating Systems

Schedule, syllabus and examination date

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.

Admission

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.

Prerequisites

Formal prerequisite knowledge

In addition to fulfilling the Higher Education Entrance Qualification, applicants have to meet the following special admission requirements:

  • Mathematics R1 or Mathematics (S1+S2)

The special admission requirements may also be covered by equivalent studies from Norwegian upper secondary school or by other equivalent studies. Read more about special admission requirements (in Norwegian).

Recommended previous knowledge

INF2220 – Algorithms and Data Structures (continued) /INF1020 – Algorithms and data structures (discontinued) /INF 110.

Overlapping courses

Teaching

3 hours of lectures and 2 hours of problem sessions per week. Mandatory assignments must be completed during the course. Rules for mandatory assignments.

Examination

Written examination (4 hour) at the end of the semester. The mandatory assignments must be accepted prior to the exam.

Examination support material

All written og printed exam resources are allowed.

Grading scale

Grades are awarded on a scale from A to F, where A is the best grade and F is a fail. Read more about the grading system.

Explanations and appeals

Resit an examination

Students who can document a valid reason for absence from the regular examination are offered a postponed examination at the beginning of the next semester.

Re-scheduled examinations are not offered to students who withdraw during, or did not pass the original examination.

Withdrawal from an examination

It is possible to take the exam up to 3 times. If you withdraw from the exam after the deadline or during the exam, this will be counted as an examination attempt.

The subject is regarded equal to INF4230, INF220 and INF220A when practicing exam regulations.

Other

It is strongly recommended to attend the first lecture since it will be given important information.

Facts about this course

Credits
10
Level
Master
Teaching
Every spring

This course will change to INF4232 spring 2017

Examination
Every spring
Teaching language
Norwegian (English on request)