| Event |
Date |
Topic | Material |
| Lecture 1 |
4/2 |
Overview of course and introduction to formal models (9.15-12)
Lecturer: TH
|
[Slides (history), Slides (CCS), Lecture
notes, Building
a Better Bug-trap (from the Economist)]
|
| Lecture 2 |
11/2 |
CCS continued (formal semantics)
Mobility Workbench (MWB)
Lecturer: MB
|
[Slides 1-on-1 page]
[Slides 4-on-1 page]
[Introduction to MWB pdf]
[
Philippa Gardner's Lecture notes about processes (Section 1.1 and most of Section 1.2 (to Example 1 on page 12)).] Note that these notes differ slightly in notation, and that the inference rules are upside down.
|
| Hand-out 1 | 11/2 | Mandatory Exercise in Concurrency
and Synchronisation
| [exercise1.pdf]
[Solution Guide for Mandatory Exercise 1]
[Mini exercise]
|
| Lecture 3 |
18/2 |
Interference and Mutual Exclusion
Locks and Synchronisation
Lecturer: MB
|
[Slides 1-on-1 page]
[Slides 4-on-1 page]
[Synchronizing Threads from The Java Tutorial]
[Concurrency made simple (sort of)]
[Supplementary literature (not part of the curriculum) Using the New Concurrent Utility Classes in Java 5.0]
[Supplementary literature (not part of the curriculum)
Synchonization in Java]
[Supplementary literature (not part of the curriculum)
Synchronizer Framework by Doug Lea]
[Solution guide]
[Java source for exercises:
Creating Threads,
Java Synchronisation Exercise]
|
| Hand-in 1 | 23/2 | Hand in Mandatory Exercise 1 before 12:00
| |
| Lecture 4 |
25/2 |
Monitors and Semaphores
Conditional Synchronisation
Lecturer: JCG
|
[Literature
Monitor and Semaphores (including exercises)]
[Slides
Slides from the lecture]
[CCS models
CCS models from the lecture]
[Java code
Java code from the lecture]
[Programming Lab
Synchronization with monitors]
|
| Lecture 5 |
4/3 |
Deadlocks and Safety Properties
Lecturer: JCG
|
[Literature
Deadlocks and Safety Properties (including exercises)]
[Slides
Slides from the lecture]
[Auxiliary litt. Process Algebra]
[CCS models
CCS models from the lecture]
[Programming Lab
Dining Philosophers in Deadlock]
|
| Hand-out 2 | 4/3 | Mandatory Exercise in Conditional Synchronisation, Safety and Liveness Properties
| [exercise2.pdf] |
| Lecture 6 |
11/3 |
Liveness Properties, Fairness
Readers/Writers Problem
Lecturer: JCG
|
[Literature
Liveness and Fairness (including exercises)]
[Slides
Slides from the lecture]
[CCS models
CCS models from the lecture]
[Java code
Java code from the lecture]
|
| Hand-in 2 | 16/3 | Hand in Exercise 2 before
12:00 | |
| Lecture 7 |
18/3 |
An application of process models
Lecturer: JCG
|
[Literature
The Needham-Schroeder Public Key Protocol - How to Break It]
[Slides
Slides from the lecture]
[CCS models CCS models from the lecture]
|
| Holiday | 25/3 | Easter | |
| Lecture 8 |
1/4 |
Distributed Systems
Pi-calculus
Lecturer: MB
|
[Slides 1-on-1 page]
[Slides 4-on-1 page]
[Literature
An Introduction to the
Pi-Calculus, Section 1 - 3.6 (section 3.3 - 3.6 can be read cursorily)]
[Supplementary literature What's in a name?]
|
| Hand-out 3 | 4/4 | Mandatory Exercise in Dynamic and Distributed Systems
| [exercise3.pdf] |
| Lecture 9 |
8/4 |
Behavioural equivalences and
A cryptographic variant of the pi-calculus
Lecturer: MB
|
[Slides 1-on-1 page]
[Slides 4-on-1 page]
[Literature Process Algebra, Section 3-3.2 (pp. 8-13) the last part on HML is cursory
An Introduction to the Pi-Calculus, Section 4, 5.4, and 6 (pp. 25-28, 35-36, 39-42) and all the sections from the last lecture
A Calculus for Cryptographic Protocols: The Spi Calculus]
|
| Hand-in 3 | 13/4 | Hand in Exercise 3 before 12:00 | |
| Lecture 10 |
15/4 |
Dichotomies and Expressiveness of Models for Mobility:
Higher-order, Locations and Linearity
Lecturer: TH
|
[Literature Expressing
Mobility in Process Algebras:
First-Order and Higher-Order Paradigms (Sec 1.1-1.2, pp.1-9)(pdf) (Sangiorgi's PhD)]
[Local
Area pi-calculus (Sec. 1-2 and 7)(pdf) (Express 2001)]
[
A CPS Encoding of Name-Passing in Higher Order Mobile Embedded
Resources (Sec. 1-2)(pdf)] (Express 2004)
[Mobile
Ambients (Sec. 1-2)] (Journal of TCS 2000)
[Slides
Slides 4-on-1 page]
[Supplementary literature
Tom Chothia. The Local Area pi-Calculus. PhD thesis, Edinburgh University, 2002.
]
|
| Hand-out 4 | 15/04 | Mandatory Exercise
in Higher-order and Locations
| [exercise4.pdf] |
| Lecture 11 |
22/4 |
Holiday
| |
tr>Hand-in 4 | 27/4 | Hand in Exercise 4 before 12:00
in pigeon hole of Thomas Hildebrandt, 4C | |
| Research Pearl | 28/04 | 15:00-16:00, Robin
Milner: "Anarchical Computing". Taking his point of departure in
the ongoing UK Grand Challenges Exercise, Robin Milner will reflect on the possibilities of establishing a science for global computing. | Seminar at ITU, Auditiorium 3 |
| Lecture 12 | 29/4 | A Distributed eXtensible Process Calculus, Bigraphs
and Reactive XML
Lecturer:
TH | [Literature
Distributed Reactive XML]
[
Reactive XML Poster]
[
Slides]
|
/IMDD
/Lecture Plan
