General

326.0VR/326.076, Time: Monday, 8:30-10:00, Room: S2 Z74, Start: March 6, 2023.

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 participate in the course, you have to register in the KUSSS System. Since the assignments will be uploaded in Moodle, you also have to create an account in the RISC Moodle (press the button "Create new account", you have to register with your jku.at email address) and self-enrol in the course (press the button "Enrol me"); then you also receive all messages posted in the course forums per email.