| date |
topic + slides |
problems |
| 6/2 |
Introduction,
Theory: Timed automata
|
- |
| 7/2 |
Practicum 15.45-17.30, HG01.057: Practice with Uppaal tool by studying
A First Introduction to Uppaal
and working on some assignments
|
train crossing,
two process race,
assignents from course for high school students
|
| 13/2 |
No meeting |
- |
| 14/2 |
Theory: timed automata;
application: Biphase Mark Protocol
|
race.xml,
race.q,
solutiontraincrossing.xml,
solutiontraincrossing.q
|
| 20/2 |
Theory: Symmetry in Uppaal,
Application: Zeroconf protocol |
- |
| 21/2 |
No meeting |
Peterson's mutex algorithm |
| 27/2 |
Theory: As Cheap as Possible: Linearly Priced Timed Automata
|
- |
| 28/2 |
Discussion of solution Peteron's mutex assignment, discussion about content first large homework assignment |
- |
| 6/3 |
Theory: Timed Games and Uppaal Tiga,
Application: Scheduling Printers |
- |
| 7/3 |
No meeting; lecturer available in office to discuss first homework assignment |
- |
| 13/3 |
Theory: LTSs and Invariants |
- |
| 14/3 |
No meeting; lecturer available in office to discuss first homework assignment |
- |
| 20/3 |
Theory: Invariants (cnt) and Simulation Relations (see also this
article) |
- |
| 21/3 |
Individual meetings with the groups to discuss progress with first assignment |
- |
| 27/3 |
Theory: Simulations (cnt);
Application: Leader election in IEEE 1394 |
Proving invariants |
|
| 28/3 |
No meeting |
- |
| 3/4 |
No meeting |
- |
| 4/4 |
No meeting |
- |
| 10/4 |
No meeting |
- |
| 11/4 |
No meeting |
- |
| 17/4 |
Theory: Linear and Branching Temporal Logics
(see also Sections 5.1, 6.1, 6.2 and 6.8 of Baier & Katoen) |
- |
| 18/4 |
Exercises CTL |
assignments 6.2, 6.4 and 6.5 from Baier & Katoen |
- |
| 24/4 |
Model Checking |
- |
| 25/4 |
Exercises CTL |
assignments 6.15 and 6.16 from Baier & Katoen |
| 1/5 |
No meeting |
- |
| 2/5 |
No meeting |
- |
| 8/5 |
Theory: Hybrid Automata
(see also original paper and
paper on LEGO case study) |
- |
| 9/5 |
No meeting |
- |
| 15/5 |
Discussion of solutions first homework assignment |
- |
| 16/5 |
Discussion of solutions first homework assignment; presentation of second homework assignment |
- |
| 22/5 |
Theory: Bounded Model Checking
(see also original paper) |
- |
| 23/5 |
No meeting (instructor available in office in case of questions) |
- |
| 29/5 |
No meeting |
- |
| 30/5 |
No meeting |
- |
| 5/6 |
No meeting |
- |
| 6/6 |
No meeting |
- |
| 12/6 |
Discussion of solutions second homework assignment; presentation third homework assignment |
- |
| 13/6 |
No meeting |
- |
| 19/6 |
Discussion of solutions second homework assignment |
- |
| 20/6 |
No meeting |
- |