Direkt zum InhaltDirekt zur SucheDirekt zur Navigation
▼ Zielgruppen ▼

Humboldt-Universität zu Berlin - Mathematisch-Naturwissenschaftliche Fakultät - Software Engineering

Softwareverifikation

 


 

Wann und Wo

Vorlesung: Mittwoch, 13-15, RUD 25, 3.113

Vorlesung: Donnerstag, 13-15, RUD 25, 3.113

Übung: Mittwoch, 15-17, RUD 25, 3.113

Wer

Dozent: Prof. Holger Schlingloff / Dr. Thomas Vogel

Beschreibung und Aufbau der Lehrveranstaltung

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.

Vorlesungsplanung bis Semesterende (Änderungen möglich)

  • Einführung
  • Aussagenlogik
  • Modellierung
  • Temporale Logik (LTL, CTL, CTL*)
  • Algorithmen zur Modellprüfung
  • Symbolische Zustandsraumrepräsentation (BDDs)
  • Abstraktion und Verfeinerung
  • Realzeit-Modellprüfung
  • Probabilistische Systeme
  • Software Model Checking

 

Skript und Übungsaufgaben

Alle Materialien zur Vorlesung werden in Moodle zur Verfügung gestellt. Das Passwort zum Kursbeitritt wird in der ersten Veranstaltung bekanntgegeben.

Änderungen an den Terminen und am genauen Inhalt sind (auch kurzfristig) möglich, werden aber im Normalfall auf dieser Webseite und in der Vorlesung bekanntgegeben.

Die Übungsblätter werden spätestens in der dem Übungstermin vorausgehenden Woche in Moodle zur Verfügung gestellt. Dort befinden sich auch die Folien zu den Übungen.

Voraussetzungen und Prüfung

Grundlagenkenntnisse in Logik und Graphtheorie werden vorausgesetzt.

Für die Zulassung zur Prüfung ist ferner die Teilnahme am Übungsbetrieb verpflichtend.

Die Lehrveranstaltung wird mit entweder eine mündliche Prüfung (etwa 30 Minuten) oder einer 180-Minuten schriftlichen Klausur geprüft. Für schriftliche Prüfungen ist ein beidseitig beschriebener (auch maschinell) DIN A4 Zettel als Zugelassenes Hilfsmittel erlaubt.

Literatur

  • Principles of Program Analysis . Flemming Nielson, Hanne Riis Nielson, Chris Hankin.
  • Modern compiler implementation in Java, Andrew Appel, 2nd. edition.
  • Edmund M. Clarke, Orna Grumberg, Doron Peled. Model Checking. MIT Press, 2000.
  • Jeff Magee and Jeff Kramer. Concurrency: State Models & Java Programs. John Wiley & Sons, 2000.
  • Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008