inf205 - Formale Methoden Eingebetteter Systeme (Vollständige Modulbeschreibung)

Keine

Das Modul vermittelt einen Überblick über semantische Modelle für reaktive Systeme, Echtzeitsysteme und hybride Systeme, sowie Beispiele für entsprechende Spezifikationslogiken. Es erläutert zustandsexplorative Verifikationsverfahren sowohl expliziter wie symbolischer Form. Die erworbenen Kenntnisse können überall eingesetzt werden, wo es um die Entwicklung zuverlässiger Software- und Hardwaresysteme geht.
Fachkompetenzen
Die Studierenden:

• beurteilen die Tragweite der mit formalen Methoden gewinnbaren Zertifikate fundiert
• beurteilen die Eignung verfügbarer Verifikationswerkzeuge für eine partikuläre Fragestellung und Systemklasse
• verwenden diese Werkzeuge an realen Systemen, interpretieren die erzielten Ergebnisse und verbessern in der Folge das untersuchte System zielgerichtet
• bereiten Systemmodelle für automatische Analyseverfahren vor und abstrahieren bzw. kodieren diese symbolisch (oder anderweitig) entsprechend
• konzipieren und implementieren eigene Verifikationsalgorithmen

Methodenkompetenzen
Die Studierenden:

• beherrschen die mathematische Modellierung komplexer und heterogener Systeme
• kennen einschlägige mathematische Modelle dynamischer Systeme und können diese auf neue Problemklassen instanziieren

Sozialkompetenzen
Die Studierenden:

• entwickeln und implementieren im Team grundlegende Algorithmen der automatischen Verifikation
• diskutieren die Vor- und Nachteile algorithmischer Alternativen und unterschiedlicher Formalisierungen

Selbstkompetenzen
Die Studierenden:

• erkennen ihr fachliches und methodisches Verständnis
• reflektieren ihre Lösungskompetenz unter Einbezug der vorgestellten Verfahren und Methoden

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 diesem Modul 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 erläutert und in ihrer Anwendung gezeigt.

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.

In der Vorlesung werden die semantischen, logischen und algorithmischen Grundlagen der automatischen Analyse eingebetteter Softwaresysteme vermittelt. Die primäre Unterweisungsform ist hierbei der medial unterstützte Vortrag sowie das didaktische Frage-Antwort-Spiel, wobei als unterstützende Medien Präsentationen, Animationen und Werkzeugvorführungen dienen.

In den Übungen wird das in der Vorlesung erworbene Wissen vertieft und praktisch umgesetzt. Hierzu werden in der ersten Semesterhälfte zweiwöchentlich Übungsaufgaben gestellt, deren Bearbeitung in Kleingruppen zur eigenverantwortlichen Prüfung des Themenverständnisses und zum partnerschaftlichen Lernen anhält.

In der zweiten Semesterhälfte wird eine ebenfalls in Kleingruppen von jeweils 3 Studierenden zu bearbeitende größere Werkzeugentwicklungsaufgabe gestellt, deren Bearbeitung die gesamte Semesterhälfte einnimmt und die Möglichkeit des projektorientierten Lernens bietet. Die Übung dient in dieser Phase der Konsultation mit den Lehrenden; insbesondere werden Lösungsansätze und Probleme vorgestellt und diskutiert.

• Michael Huth, Mark Ryan: Logic in Computer Science: Modelling and Reasoning About Systems. Cambridge University Press, 2004.
• Christel Baier, Joost-Pieter Katoen: Principles of Model Checking. MIT Press, 2008.
• Edmund M. Clarke, Orna Grumberg, Doron A. Peled: Model Checking. MIT Press, 2000.

1. Termin: Abgabe des Semesterprojekts inkl. schriftlicher Ausarbeitung eine Woche nach Ende der Vorlesungszeit; anschließend Kolloquium und Abschlussgespräch

2. Termin: Wiederholung der Abgabe des Semesterprojekts inkl. schriftlicher Ausarbeitung zwei Wochen vor Beginn des Folgesemesters anschließend Kolloquium und Abschlussgespräch

Projekt
Die Prüfungsarbeit besteht aus einem Semesterprojekt sowie dessen Verteidigung in einem Abschluskolloquium