INF4231 – Formal Modelling and Analysis of Communicating Systems
Course description
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
- 10 credits overlap with INF3230 – Formal modeling and analysis of communicating systems (continued)
- 10 credits overlap with INF4230 – Formal modeling and analysis of communicating systems (discontinued)
- 10 credits overlap with INF220
- 9 credits overlap with INF220A
- 3 credits overlap with IN307
- 9 credits overlap with INF3232 – Logic for System Analysis (continued)
- 9 credits overlap with INF4232 – Logic for System Analysis (continued)
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.