Formal Models of Parallel and Distributed Systems (SS 2021)

326.0VR/326.076, Time: Monday, 8:30-10:00, Zoom. Start: March 8, 2021.

This course deals with the formal modeling and specifying of concurrent systems such as parallel or multi-threaded programs, distributed hardware and software systems, mobile systems, and the like. We will discuss two major approaches:

• The state-oriented approach which focuses on the sequence of states that a system has at any time. In essence, the model describes the transitions of the system from one state to another; we are interested to verify whether the resulting state sequence satisfies a specification formula. Representatives of this approach are RISCAL system models and Lamport's Temporal Logic of Actions (TLA) on which the specification language TLA+ is based.
• The communication-oriented approach which focuses on the sequence of communication operations in which a system may engage at any time. In essence, the model describes the flow of messages among the components of the system; we are interested to verify whether the resulting interaction behavior conforms to that of some specification system. A representative of this approach is Milner's Calculus of Communicating Systems (CCS) for modeling communication and concurrency and its successor, the pi-Calculus, which also models mobility.

Our discussion will be accompanied by the demonstration of practical software tools supporting these calculi. The participants are expected to elaborate small exercises which will be used for grading (there will be no final exam).

To take part in the course, you have to enrol in the KUSSS system. Since the exercises will be submitted via Moodle, you also have to login in Moodle and register as a course participant. You will then also receive per email all messages posted in the Announcements forum and may yourself post messages in the Questions and Answers forum.