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.