Planning Course Analysis of Embedded Systems, Slides, Problems and Solutions

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: Symmetry in Uppaal, Application: Zeroconf protocol -
16/2 Solutions to problems 9/2, presentation of first homework assignment -
21/2 and 23/2 No meeting (Carnaval break) -
28/2 Theory: As Cheap as Possible: Linearly Priced Timed Automata -
1/3 No meeting; lecturer available in office to discuss first homework assignment -
6/3 Theory: LTSs and Invariants -
7/3 No meeting; lecturer available in office to discuss first homework assignment -
13/3 Theory: Simulation Relations (see also this article) and Compositional Abstraction in Uppaal -
15/3 No meeting; lecturer available in office to discuss first homework assignment -
20/3 Theory: Linear and Branching Temporal Logics (see also Sections 5.1, 6.1, 6.2 and 6.8 of Baier & Katoen) -
22/3 No meeting -
27/03 Theory: Model Checking assignments 6.2, 6.4 and 6.5 from Baier & Katoen
3/4 and 5/4 No meeting -
10/4 and 12/4 No meeting -
17/04 and 19/04 No meeting -
24/4 and 26/4 Assignments 6.2, 6.4 & 6.5 from Baier & Katoen, Presentation Second Homework Assignment -
1/5 and 3/5 No meeting -
08/05 Theory: Probabilistic models DTMCs
10/5 Evaluation First Assignment + Discussion Second Assignment -
15/05 Theory: Markov Decision processes -
18/5 and 22/5 No meeting -
24/05 Case Study: IEEE Firewire; Tools: PRISM -
29/05 TBD -
31/5 Visit to NXP; discussion Second Assignment -
05/06 Guest lecture on Deadlock Verification in Network-on-Chip by Julien Schmaltz -

Homework Assignments 2012

available completed problem
28/02 05/04 Assignment 1: Uppaal
24/04 29/05 Assignment 2: Modelling and Analysis of Strip Handling in a Die-Bonder Strip Glue Machine Using nuSMV2
29/05 01/07 Assignment 3: PRISM

Last change made on 18/5/2012 by Frits Vaandrager.