inf205 - Formale Methoden Eingebetteter Systeme (Vollständige Modulbeschreibung)
Modulbezeichnung | Formale Methoden Eingebetteter Systeme |
Modulkürzel | inf205 |
Kreditpunkte | 6.0 KP |
Workload | 180 h |
Einrichtungsverzeichnis | Department für Informatik |
Verwendbarkeit des Moduls |
|
Zuständige Personen |
|
Teilnahmevoraussetzungen | Keine |
Kompetenzziele | 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:
Methodenkompetenzen Die Studierenden:
Sozialkompetenzen Die Studierenden:
Selbstkompetenzen Die Studierenden:
|
Modulinhalte | 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. |
Literaturempfehlungen |
|
Links | |
Unterrichtsprachen | Deutsch, Englisch |
Dauer in Semestern | 1 Semester |
Angebotsrhythmus Modul | jährlich |
Aufnahmekapazität Modul | unbegrenzt |
Lehr-/Lernform | V+Ü |
Vorkenntnisse | Fundierte Grundkenntnisse in mathematischer Logik, diskreter Mathematik, Automaten- und Berechenbarkeitstheorie, wie sie in den Modulen "Diskrete Strukturen" und "Theoretische Informatik I + II" vermittelt werden. Zudem Programmierkenntnisse, wie sie im "Programmierkurs" erworben werden. Begründung: Die in der Vorlesung vorgestellten Verfahren basieren auf einer Operationalisierung von Semantik durch Reduktion auf logische Kodierungen und mechanisierte Prüfung logischer Aussagen. Ein Verständnis dieser Inhalte sowie ihre werkzeugtechnische Umsetzung bedarf der Grundlagen aus den vorgenannten Veranstaltungen. |
Lehrveranstaltungsform | Kommentar | SWS | Angebotsrhythmus | Workload Präsenz |
---|---|---|---|---|
Vorlesung | 3 | WiSe | 42 | |
Übung | 1 | WiSe | 14 | |
Präsenzzeit Modul insgesamt | 56 h |
Prüfung | Prüfungszeiten | Prüfungsform |
---|---|---|
Gesamtmodul | 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 |