Hybride Systeme

AS 303: Formale Methoden Eingebetter Systeme (SoSe 2010)

Stud.IP: "Formale Methoden Eingebetteter Systeme"

Lehrende:

Prof. Martin Fränzle, Stefan Puch, Gerald Sauter

Veranstaltungsform:

3 VL + 1 Ü (Übungen zweistündig alle zwei Wochen)

Zeiten und Räume:

 

  • Mo, 08:00 - 10:00 (Vorlesung)
    Raum: A05 1-160
  • Mi, 10:00 - 12:00 (Vorlesung / Übung)
    Raum: A05 1-160

Inhalte des Moduls:

Eingebettete Computersysteme stehen in ständiger Interaktion mit ihrer Umgebung, was zu schwer vorhersehbaren Interaktionssequenzen führen kann. Dieser Umstand erschwert Konstruktion und Validation derartiger Systeme. Vergleichbar dem Einsatz statischer und materialkundlicher Modelle in der Bauwirtschaft sind deshalb formale Modelle für verschiedene Aspekte -z.B. Ausführungszeit, Energiebedarf, mögliche Systemdynamik- eingebetteter Systeme entwickelt worden. Diese stellen den jeweiligen Aspekt des Systems in geschlossener Form dar und erlauben damit die -oft vollautomatische- Herleitung von verlässlichen Kenndaten und Zertifikaten, welche für jedes beliebige Interaktionsszenario mit der Umgebung gelten. Dies steht im Gegensatz zu Methoden des Testens oder Profilings, welche nur ausgewählte Szenarien prüfen und somit nur eine begrenzte Überdeckung bieten können.

In der Vorlesung werden verschiedene derartige Modelle erklärt und Methoden zur vollautomatischen Analyse -d.h. Herleitung von Kenndaten oder Zertifikaten- oder Synthese -d.h. automatischen Erzeugung korrekter Systementwürfe- aus derartigen Modellen gezeigt werden.

In den Übungen besteht die Möglichkeit, die entsprechenden Kenntnisse durch Hands-on-Erfahrung mit domänentypischen Modellierungs- und Verifikationswerkzeugen zu vertiefen, sowie in einem geführten Prozess ein (kleines) vollautomatisches Verifikationswerkzeug selbst zu erstellen.

Ziele des Moduls:

Grundkenntnisse in der Mathematischen Modellierung und Verständnis der automatischen Verifikation Eingebetteter Systeme.