Anwendung formaler Methoden in der Entwicklung von eingebetteten Systemen


Inhalt


In diesem Seminar werden Systeme behandelt, deren Verhalten nicht nur durch die Veränderung diskreter Zustände, sondern auch kontinuierlicher Parameter bestimmt ist. Hierzu gehören Parameter wie die linear fortschreitende Zeit („timed systems“) oder Größen wie Temperatur, die z.B. durch Differentialgleichungen beschrieben werden („hybrid systems“).

Es wird zum einen die Modellierung derartiger Systeme betrachtet, zum anderen aktuelle Ansätze zur algorithmischen Verifikation und Synthese, insbesondere in Hinblick auf deren Anwendungspotential. Themen sind u.a.:

  • Hybride Systeme und Zeit-Automaten
  • Model-Checking
  • Simulation
  • Algorithmische Synthese (Spieltheorie, Supervisory Control Theory)


Themen


  • 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


Ablauf


Dieses Seminar wird als Blockseminar durchgeführt. Das erste Treffen wird am Ende der vorlesungsfreien Zeit oder zum Beginn des Wintersemesters durchgeführt. Das Blockseminar wird dann im Februar 2008 an zwei aufeinander folgenden Tagen abgehalten. Zwischendurch wird es einige Deadlines zur Abgabe der schriftlichen Ausarbeitung und der Folien geben, die eingehalten werden müssen.

Termine


  • Vorbesprechung: 15.10.2007, 16Uhr, Raum 2323
  • Vorträge: 14./15.02.2008


Anforderungen


  • Teilnahme an allen Terminen
  • Eigenständige Einarbeitung in das gegebene Thema
  • Schriftliche Ausarbeitung von 10-15 Seiten / Person in der von uns zur Verfügung gestellten Vorlage
  • Vortrag von 30 Minuten (strikt) / Person
  • Deadlines strikt (Es genügt die Dateien per E-Mail zu schicken. Kein Schein bei zweimaligem Verpassen der Deadlines!):
    • 10.11.07: zusätzliche Literatur
    • 30.11.07: Gliederung und kurze Inhaltsangabe zu jedem Abschnitt
    • 10.01.08: schriftliche Ausarbeitung & Folien
  • Die Ausarbeitung und die Folien müssen selbstständig verfasst werden. Alle benutzten Quellen und Hilfsmittel müssen angegeben sowie Zitate kenntlich gemacht werden.


Unterlagen

Kontakt


  • Gerlind Herberich
Diese Website verwendet Cookies. Durch die Nutzung der Website stimmen Sie dem Speichern von Cookies auf Ihrem Computer zu. Wenn Sie nicht einverstanden sind, verlassen Sie bitte die Website.Weitere Information

RWTH Aachen - Lehrstuhl Informatik 11 - Ahornstr. 55 - 52074 Aachen - Deutschland