| date |
topic + slides |
problems |
| 31/1 |
Introduction,
Tool: Uppaal
|
- |
| 2/2 |
Practicum: Practice with Uppaal tool by studying
A Tutorial on Uppaal,
A First Introduction to Uppaal,
working on some assignments.
Play with jobsshop models:
Jobshop0.xml,
Jobshop1.xml,
Jobshop2.xml,
JobshopP.xml, and
Jobshop.q.
|
assignents from course for high school students,
two process race
|
| 7/2 |
Theory: timed automata;
application: Biphase Mark Protocol
|
- |
| 9/2 |
Work on small assignments, solution to problem 2/2
|
Peterson's algoritme,
rush hour
|
| 14/2 |
Theory: LTSs and Invariants |
|
| 16/2 |
Practicum
|
rush_hour_good_2.xml, rush_hour_good_2.q
|
| 21/2 and 23/2 |
No meetings (Carnaval break) |
- |
| 28/2 |
Theory: As Cheap as Possible: Linearly Priced Timed Automata
|
|
| 1/3 |
Presentation of first homework assignment; discussion of solution to exercises
|
|
| 6/3 |
Theory: Symmetry in Uppaal,
Application: Zeroconf protocol |
- |
| 13/3 |
Theory: Compositional Abstraction in Uppaal,
Application: Modelling Clock Synchronization in the Chess gMAC WSN Protocol |
- |
| 20/3 |
Theory: Timed Games,
Application: Adaptive Scheduling of Data Paths using Uppaal Tiga |
- |
| 27/03 |
Theory: Linear and Branching Temporal Logics
|
- |
| 3/4 and 11/04 |
No meetings |
- |
| 17/04 |
Theory: Model Checking
|
assignments 6.2, 6.4 and 6.5 from Baier & Katoen |
| 20/4, 25/4, 2/05 and 9/05 |
No meetings |
- |
| 17/05 |
Discussion of CTL assignments from Baier & Katoen |
- |
| 23/05 |
Theory: Probabilistic models |
DTMCs |
| 30/05 |
Theory: Markov Decision processes |
- |
| 06/06 |
Guest lecture on Deadlock Verification in Network-on-Chip by Julien Schmaltz |
- |
| 20/06 |
Tools: PRISM |
- |