General topic: Models, analysis and tools for embedded systems

The concrete content of the course will vary from year to year.

Main part

This year, the main part was given by:

• Professor Martin Fränzle, Department of Computer Science, Carl von Ossietzky Univeristät Oldenburg, Germany. He is a professor for hybrid-discrete systems and a member of the Interdisciplinary Research Center for Safety-Critical Systems. He is also a guest professor at IMM, DTU, funded by the Velux Fonden.
• Simon Perathoner, Nikolay Stoimenov and Wolfgang Haid, Swiss Federal Institute of Technology Zurich Computer Engineering and Networks Laboratory.
• Arne Hamann and Razvan Racu, Institute of Computer and Communication Network Engineering, Technische Universität Braunschweig.

Form

The course this year was partitioned into three periods:

• First period (4/6 - 8/6, 4 days as 5/6 is a holiday):
   Lectures by Martin Fränzle and lab sessions.
   Lecture 1, Lecture 2, Lecture 3-4, Lecture 5, Lecture 6, Lecture 7, Lecture 8. Article 1, Article 2.
   New version of HySat is uploaded here (which fixes old bugs concerning integer arithmetics).
   In the lectures, we will introduce a comprehensive set of state-based models as well as automatic procedures for their analysis. The exercise classes will complement this by providing hands-on experience with appropriate verification tools. Keywords: Finite-state systems, computation tree logic (CTL), CTL model checking, symbolic methods, SAT solving, hybrid discrete-continuous automata models, verification by approximation, satisfiability of large arithmetic formulae.
• Second period (11/6 - 12/6):
   Lectures by Simon Perathoner, Nikolay Stoimenov and Wolfgang Haid on Modular Performance Analysis with Real Time Calculus, and hands-on exercises with RTC.
  Slides
   Lectures by Arne Hamann and Razvan Racu on Symbolic Timing Analysis for Systems (SymTA/S), a system-level performance and timing analysis approach based on formal scheduling analysis techniques and symbolic simulation, and hands-on exercises with SymTA/S. Slides
• Third period (12/6 - 25/6):
   Project work, which might concern be building keypress verification tool yourself within a guided process.
   The students may complete this project at their home institution and hand in the required material no later than June 25, 2007.

Diplomas

Two kinds of diplomas were issued: one kind for completion of the first two periods, and another for successful completion of all three periods, including the project.

Responsible Teachers

All Informatics and Mathematical Modelling, Technical University of Denmark.

• Michael R. Hansen
• Jan Madsen
• Hans Henrik Løvengreen

Réalisation Axome - Création de sites Internet