Formal Models of Parallel and Distributed Systems (SS 2011)
Abschnittsübersicht
-
Formal Models of Parallel and Distributed Systems (326.076, SS 2011)
Time: Monday, 8:30-10:00. Room: T 038/1. Start: March 7, 2011.
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. A representative of this approach is 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.
-
The Temporal Logic of Actions (TLA)
- Leslie Lamport: Introduction to TLA
- Leslie Lamport: Specifying Concurrent Systems with TLA+
- The Temporal Logic of Actions I
- The Temporal Logic of Actions II
- Leslie Lamport: The Temporal Logic of Actions
- Leslie Lamport: Specifying Systems (Amazon page).
TLA+ Tools
- Leslie Lamport: Introduction to TLA
-
The Calculus of Communicating Systems (CCS)
- The Calculus of Communicating Systems
- Luca Aceto et al: Reactive Systems: Modeling, Specification, and Verification
- Robin Milner: Communication and Concurrency (Amazon page)
- FSP Quick Reference
- Concurrency: State Models and Java Programs
- FSP Language Specification (restricted)
- Processes (restricted)
- Concurrency (restricted)
-
The pi-Calculus
- The pi-Calculus (Part 1) (4 on 1)
- The pi-Calculus (Part 2) (4 on 1)
- Elements of Interaction (restricted)
- Robin Milner: The Polyadic pi-Calculus: a Tutorial
- Robin Milner: Communicating and Mobile Systems: the pi-Calculus (Amazon page)
- M. Carbone et al: Structured Global Programming for Communication Behaviour
- From the pi4soa project
-
Course Software
I recommend to download the VirtualBox virtual machine for using the tools presented in this course. -
Exercises
Grading will be based on three to four exercises.