02917 Advanced Topics in Embedded Systems (June 2010).
DTU Study handbook: Description
Supported by ARTIST - Network of Excellence on Embedded Systems Design.
Models, analysis and tools for embedded
systems. The concrete content of the course will vary from year to
year. Previous years' courses are described here: 2007, 2008, 2009
The course will be given by:
- Jüri Vain, Department of Computer Science, Tallinn University of Technology, Estonia. His research interests are within the development and usage of formal methods in real-time and hybrid systems, model-based test generation, programming theory, etc.
- Anton Cervin, Automatic Control, Lund Univeristy. His research interests include real-time control systems, controller implementation issues, event-based and networked control systems, real-time scheduling theory, and computer tools for analysis and simulation of controller timing.
- Kokichi Futatsugi, Japan Advanced Institute of Science and Technology. His research interest includes: Formal Methods, Formal Specification Languages, Systems Verification, System Security and Safety, Concurrent and Cooperative systems, Software Engineering.
- Michael R. Hansen, DTU Informatics, Technical University of Denmark. His research interests includes: Formal methods in embedded systems and software engineering, model-based approaches, real-time systems, logic and semantics, functional programming, verification and model checking.
The course is this year partitioned into five
First period (14/6 - 15/6): Lectures by Jüri Vain on Model-Based Development and Validation of Multirobot Cooperative
System. Further description is found here. This part will contain a mix of lecturing and hands-on exercises especially
built around the Uppaal tool suite. Slides: Lecture 1,
Lecture 2, Lecture 3, Exercise 1
- Second period (16/6 - 17/6): Lectures by Anton Cervin on Simulation of Networked Embedded Control Systems Using TrueTime. TrueTime is a MATLAB/Simulink-based simulator that has been developed at Lund University since 1999. It provides models of multi-tasking real-time kernels and networks that can be used in simulation models of networked embedded control systems. The lectures will start with an introduction to embedded and networked control aimed at computer science students. The features of the simulator will be described, together with many examples. Each day will end with a computer simulation exercise. Slides: Lecture 1,
Lecture 2, Lecture 3
- Third period (18/6): A logical approach to modelling and analysis of resource constraints. Lectures are Michael R. Hansen. Slides: Lecture 1, Lecture 2, Lecture 3
- Forth period 21/6 - 22/6: Lectures by Kokichi Futatsugi on Specification and verification with proof scores in CafeOBJ. CafeOBJ is a most advanced algebraic formal specification language system with rewriting/reduction engine which can be used for interactive verification. Proof scores are scripts for verifications and provide versatile ways to prove properties of specifications. The lecture gives foundations and techniques of CafeOBJ and proof scores by using elementary examples of natural numbers, lists, etc. Material is found here
- Fifth period starting 23/6:
Project work. The students may complete this project at their home institution and hand in the required
material no later than July 9, 2010.
Two kinds of diplomas are issued: one kind for completion of the first four periods (workload corresponds to 2.5 ECTS),
and another for successful completion of all four periods, including the project (workload corresponds to 5 ECTS).
Lectures:The lessons takes place at DTU Informatics. First lecture starts
Monday, June 14, at 9:00 am.
Michael R. Hansen
Jan Madsen (firstname.lastname@example.org), and Hans Henrik
Løvengreen, (email@example.com), all DTU Informatics, Technical University of Denmark.
Send email to Michael R. Hansen
(firstname.lastname@example.org) no later than Tuesday, June 1.
There is a limited number of travel grants for students coming from institutions outside of Denmark.. To apply for a grant, send email to Michael R. Hansen
(email@example.com) with personal information (name, affiliation, ph.d. supervisor, title of project, ect.
and a budget).
Accommodation:You may have a look at:
Travel information:You may have a look at:
Last update: May 05, 2010, Michael R. Hansen