Administration
Course starts on 4th of April 2000, 10-12.
Examination
To receive 4 credit points two batches of exercises have to be solved
and presented at the exercises sessions (see the schedule below).
Exercises
Literature
and course notes
Alternative readings:
Links
Schedule
All meetings are on Tuesdays 10-12, in Eliten.
-
4 April: Introduction [JM] (transparencies)
-
Motivation: modeling of concurrent communicating systems and automatic
verification of the models. General discussion about the approach. Modelling
language: CCS. What are models. Checking equivalence of models: kinds of
equivalences considered. Properties to be described, specification languages:
mu-calculus, CTL. Correctness of a model wrt specification. The verification
system. Pi-calculus: extending CCS for modeling mobility.
-
11 April: Reactive sequential processes [JM] (transparencies)
-
From Finite Automata to Reactive Systems. Why the concept of equivalent
FA is not suitable for comparing reactive systems. (Chapter 2).
-
Labeled transition systems (LTS). Nondeterministic sequential processes
and strong bisimulation (Chapter3).
-
18 April: Concurrent communicating systems [JM] (transparencies)
-
Interacting sequential processes: labels and synchronizations. The process
description language: syntax and semantics. (Chapter 4). A comment on value-passing
CCS.
-
Structural equivalence, Strong bisimulation for concurrent processes, Strong
equivalence (Chapter 4, 5).
-
2 May: Observational equivalence [JM] (transparencies)
-
What we can observe? Weak bisimulation. Observational equivalence. Examples.
(Chapter 6, 7)
-
9 May: Model checking with mu-calculus [UN] (transparencies)
-
A general view of model checking. Introduction to mu-calculus. mu-calculus
and temporal logic. Examples of model checking in CWB. A taste of CTL --
another temporal specification language.
-
16 May: Student presentations
-
Homework 1
-
23 May: Introduction to Pi-calculus [JM] (transparencies)
-
Motivation: describing mobility in CCS style (Chapter 8). A survey of Pi-calculus
(Chapter 9). Selected examples (Chapter 10)
-
30 May: No lecture
-
6 June: Student presentations
-
Homework 2
-
|