Software-Verifikation

Modulnummer: W09-01
Englischer Titel: Software Verification
Leistungspunkte: 9
Lehrperson: Schlingloff

Empfohlene Vorkenntnisse

Logik in der Informatik
Software Engineering

Zwingende Voraussetzungen

- keine -

Inhalt

Je mehr Software in sicherheitskritischen Systemen eingesetzt wird, umso wichtiger wird es, ihre Korrektheit objektiv nachzuweisen. Beispiele sind Signalisierungsanlagen in der Bahntechnik, Steuercomputer in Flugzeugen oder Regelungen medizinischer Geräte. In den letzten Jahren sind formale Verifikations- und Analysemethoden für solche Software so weit entwickelt worden, dass sie auch für industriell relevante Probleme einsetzbar geworden sind. Zu den Eigenschaften, die formal nachweisbar sind, gehören z.B. die Abwesenheit von arithmetischen Überläufen bzw. Nulldivisionen, Speicherfehlern, oder „toten“ Codes. Der Einsatz dieser Methoden wird von den einschlägigen Normen für hochgradig sicherheitsrelevante Software dringend empfohlen. Aber auch bei der Entwicklung von Treibern und Standardsoftware für weitverbreitete Betriebssysteme werden statische und dynamische Analysewerkzeuge eingesetzt.
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: 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.
Die Vorlesung gibt einen Überblick über die wichtigsten formalen Methoden zur Software-Verifikation. In den Übungen erlernen die Teilnehmer anhand verschiedener Werkzeuge, wie die entsprechenden Methoden in der Praxis eingesetzt werden können.

Dieses Modul kann nicht gemeinsam mit den Modulen W5-2 oder W5-4 eingebracht werden.

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

Aktive Teilnahme an Vorlesung und Übung, regelmäßige Bearbeitung der Übungsaufgaben
sowie Vorstellen eigener Lösungen

Lehrveranstaltungen

Vorlesung: 4 SWS
Übung: 2 SWS

Forschungsorientiert

nein

Angeboten für Studiengänge

Monobachelor: ja
Kombinationsbachelor: ja
Infomit: ja

Angeboten im

Wintersemester: nein
Sommersemester: nein

Turnus

Unregelmäßig