Application of Formal Methods in Embedded Systems Development


This seminar deals with the so-called hybrid systems. The characteristics of these systems are not only determined by transitions between discrete states but also by continuous parameters. Examples for such parameters are time or temperature being described by means of differential equations. A typical example for a hybrid system is a digital controller of an analog plant.

On the one hand, the modelling of such systems will be considered, on the other hand state-of-the-art approaches for the algorithmic verification and synthesis. Here, application potential of those approaches is of particular interest.

Topics are amongst others:

  • Hybrid systems and timed automata
  • Model-Checking
  • Simulation
  • Algorithmic synthesis (Game Theory, Supervisory Control Theory)


  • The Theory of Timed Automata
  • The Theory of Hybrid Automata
  • Real-Time Model Checking
  • Model-Checking of Hybrid Systems
  • The Theory of Controller Synthesis (Game Theory & Supervisory Control Theory)
  • Controller Synthesis under Real-Time Constraints
  • Synthesis of Hybrid Control Systems
  • Modeling and Model-Checking using Hybrid Automata: Case Study “Electronic Height Control”
  • Abstraction-Based Controller Synthesis using Hybrid Automata: Case Study “Chemical Process Control”
  • Model-Checking Embedded Systems Assembly Code


This seminar is arranged as a block seminar. The first meeting will take place in the last week of the summer term or at the beginning of the winter term 07/08. The presentations will be scheduled on two consecutive days in February 2008. There will be deadlines in between that have to be met.


  • Preliminary discussion: 2007-10-15, 4pm, room 2323
  • Presentations: 2008-02-14 and 2008-02-15


  • Participation on all dates
  • Getting familiar with your topic on your own
  • Written elaboration of 10-15 pages / person using our template
  • Presentation of 30 minutes (strict) / person
  • Deadlines strict (you can send your files via email.):
    • 2007-11-10: additional literature sources
    • 2007-11-30: structure and short abstract to each section
    • 2008-01-10: written elaboration & slides
  • The elaboration and the slides must be composed by yourself only. All sources, additional aids and quotations must be indicated. Quotations must be distinguishable.


  • Paper template
  • Preliminary discussion slides (2007-10-15)


  • Gerlind Herberich
This website uses cookies. By using the website, you agree with storing cookies on your computer. If you do not agree please leave the website.More information about cookies

RWTH Aachen University - Chair of Computer Science 11 - Ahornstr. 55 - 52074 Aachen - Germany