Please register your participation here


The students should have visited the lecture "Data Networks" or "Verification".


The course will guide you through a wealth of contemporary research trends in the design of distributed systems with predictable quality of service (QoS). 

Credit Points: 6

Preliminary Schedule

The course consists of two parts.


A first preparatory part is a crash course that brings you to level for the main part if you have followed only one of the required courses.


For those that did not follow "Data Networks", we will review:

  • basic probability theory,
  • stochastic models, Markov chains,
  • protocol design fundamentals,
  • reliable data transfer.


For those who did not follow "Verification", we will review:

  • principles of model checking,
  • transition systems, Kripke structures,
  • temporal logics,
  • computation tree logic.


The preparatory part takes place February 23-25. Tentative time table:



Feb 23, R 014:

9:15 Introduction

9:45 Data Networks A

11:00 Verification A


13:30 Data Networks B

(finishes 14:30)


Feb 24, R 014:

9:15 Data Networks C

11:00 Verification B


13:30 Tutorial exercises (both!)

15:30 Data Networks D

(finishes 17:00)


Feb 25, R 014:

9:15 Data Networks E

11:00 Verification C

13:30 Tutorial exercises (both!)

(finishes 15:30)


March 1, R 528

10:30 Tutorial exercises (both!)


Here is literature for the preparatory part, apart from those listed at

DN and V:


The main part takes place March 7-18 in room SR 015.


In the main part, each day starts at 09:15 with about three lectures of 45 minutes in the morning, together with exercises held in the early afternoon every second day.


We will cover:

  • Models
    • process algebra,
    • timed automata and generalized semi-Markov processes,
    • stochastic process algebra,
    • Modest,
    • UML statecharts and extensions.

  • Model checking 
    • real-time model checking,
    • Markov model checking,
    • simulation-based model checking.

  • Applications
    • GSM-R train radio,
    • lacquer production planning,
    • universal plug-and-play protocols,
    • extasy optimisation (if time permits).


Here is how to use the MoToR/Moebius tool. The "reliable data transfer" models in MoDeST can be found here.


Prof. Dr.-Ing. Holger Hermanns

Dr. David N. Jansen

Lecture Notes

Here are the lecture notes in pdf:


Literature for the main part



Here is your homework.


Here is Figure 1 of this paper  in colour.