Anwendung formaler Methoden in der Entwicklung von eingebetteten Systemen

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)

• 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

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.

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

• 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.

• Vorlage für die Ausarbeitung
• Folien von der Vorbesprechung (15.10.07)

• Gerlind Herberich