INF4230 – Formal modeling 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
None
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
Teaching
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.
Examination
Midterm exam (app. 37%). Written examination at the end of the semester (app. 63%). Graded marks (A - F).
Other
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