Verifikation von Software

Modulnummer: Q09-06
Englischer Titel: Verification of Software
Leistungspunkte: 9
Lehrperson: Schlingloff

Empfohlene Vorkenntnisse

Softwaretechnik, Einführung in die theoretische Informatik

Zwingende Voraussetzungen

keine vorherige Teilnahme an vergleichbaren Bachelor-Modulen

Inhalt

Um sicherheitskritische Systeme in der Praxis einsetzen zu können, muss die Korrektheit der Software objektiv nachgewiesen werden. Zur Zulassung von Systemen wie etwa Signalisierungsanlagen in der Bahntechnik, Steuercomputer in Flugzeugen oder Regelungen medizinischer Geräte empfehlen die einschlägigen Normen (EN 61508, EN 50128 oder DO-178C) den Einsatz formaler Methoden. In den letzten Jahren sind formale Verifikations- und Analysemethoden so weit entwickelt worden, dass sie auch für Probleme von industriell relevanter Größe einsetzbar geworden sind. Bei der Modellprüfung (Model Checking) wird ein Modell des Systems bezüglich einer temporallogischen Eigenschaft überprüft, und bei der dynamischen Analyse werden Laufzeiteigenschaften bezüglich spezifizierter Anforderungen untersucht. Zu den Eigenschaften, die formal nachweisbar sind, gehören z.B. die Abwesenheit von arithmetischen Überläufen bzw. Nulldivisionen oder die Erreichbarkeit von Fehlerzuständen und Lokalisierung „toten“ Codes. Ein neues Gebiet ist der Sicherheitsnachweis für lernende und adaptive Systeme.
Das Modul behandelt Methoden zur deduktiven Verifikation, bei der die Beweise interaktiv vom Benutzer mit einem Beweissystem geführt werden, sowie automatische Verifikationsverfahren, die in der industriellen Praxis eingesetzt werden.
Die Vorlesung gibt einen Überblick über die wichtigsten formalen Methoden zur Software-Verifikation.
In den Übungen erlernen die Teilnehmer, wie die entsprechenden Methoden in der Praxis eingesetzt werden können. Es wird das praktische Arbeiten und der Umgang mit verbreiteten Werkzeugen der Verifikation von Software geübt.
In Abgrenzung zum Bachelor-Modul W09-01 (Software-Verifikation) geht
dieses Master-Modul auch auf neuere Techniken wie Abstraktionsverfeinerung
anhand von Gegenbeispielen, erweiterte temporale Logiken, Erfüllbarkeit
modulo Theorien und die Verifikation neuronaler Netze ein. Die Teilnahme
am Bachelor-Modul ist explizit nicht Voraussetzung für die Teilnahme
an diesem Master-Modul; eine Teilnahme an beiden Modulen ist nicht
möglich.

Erforderliche Arbeitsleistungen für LP-Vergabe und Prüfungszulassung

- schriftlich eingereichte und/oder mündlich vorgetragene Lösungen zu Aufgaben
- Erstellung von Software und/oder Hardware
- Vortrag/Vorträge der Studierenden
- aktive Teilnahme

Lehrveranstaltungen

Vorlesung: 4 SWS 4 LP
Übung: 2 SWS 4 LP
MAP: 1 LP

Zugeordneter Vertiefungsschwerpunkt

Algorithmen und Modelle: nein
Modellbasierte Systementwicklung: ja
Daten- und Wissensmanagement: nein
Ohne Vertiefungsschwerpunkt: nein

Sprache im Modul

Deutsch: ja
Englisch: ja

Angeboten für Studiengänge

M. Sc.: ja
M. Ed.: ja
Wirtschaftsmaster: ja

Angeboten im

Wintersemester: nein
Sommersemester: nein

Turnus

Unregelmäßig