Test of Distributed Systems
Handins & Exercises
Exercises/AssignmentsIn connection with most lectures we’ll spend some time on exercises. The exercises supplements and illustrates the formal presentation of the ideas in the written material read for the day. The course contains two types of exercises: a number of smaller one-lecture exercises and a single, larger assignment that runs over several weeks.
One-lecture exercisesThe one-lecture exercises follow a fixed pattern:
- Students are divided into groups with appr. 4-5 members.
- Each group works with the exercise(s) for the designated duration.
- The (possibly incomplete) results from each group, in the shape of one or more Promela programs are collected by / delivered to the instructor.
- Select programs are chosen for demonstration, and the group that made the program presents their work, explaining the ideas behind their model and demonstrating that their Promela model actually works and exhibit the desired features (such as absence of deadlocks, compliance with one or more LTL predicates etc.).