TU BRAUNSCHWEIG

Fundamente des Software Engineering (FSE)

Dozentin: Prof. Dr.-Ing. Ina Schaefer
Assistent: Remo Lachmann, M.Sc.

Aktuelles

Die Vorlesungstermine im Januar wurden aktualisiert. Die erste Vorlesung im neuen Jahr findet am 9. Januar statt.

Achtung: Die Raumangaben für die Übungen finden Sie weiter unten bei der Terminplanung.

Inhalte

Formale Methoden bezeichnen Methoden für den Systementwurf oder die Systemanalyse und Implementierungstechniken, die mit mathematischer Exaktheit beschrieben werden. Das Ziel ist es, Systeme zu konstruieren, die sich mit hoher Zuverlässigkeit gemäß ihrer Spezifikation verhalten. Diese Lehrveranstaltung führt theoretisch und praktisch die beiden wichtigsten Arten der formalen Methoden für die Analyse von Software ein: Model Checking und deduktive Verifikation.

Model Checking ist ein automatisches Verfahren zum Nachweis von Systemeigenschaften. Die Vorlesung beschäftigt sich mit folgenden Themen:

  • Theoretische Grundlagen des Model Checkings
  • Spezifikationssprachen für Systemeigenschaften
  • Automatische Verifikation mit einem Model Checker (SPIN)

Für die Einführung in die deduktive Verifikation verweden wir das KeY System, ein integriertes Werkzeug für die Spezifikation und Verifikation von Java-Programmen. Java-Programme werden mit JML Spezifikationen annotiert und in Logik übersetzt. Ein interaktiver Theorembeweiser wird dann verwendet, um die Spezifikationen für die Programme formal zu verifizieren. Die Vorlesung behandelt folgende Themen:

  • Java Modeling Language (JML)
  • Formale Semantik von Systemen
  • Prädikatenlogik für die Spezifikation von Java-Programmen
  • Übersetzung von JML in Dynamic Logic
  • Verifikation von Beweisverpflichtungen

Die Unterrichtssprache ist Deutsch (oder Englisch bei Bedarf). Java-Kenntnisse werden vorausgesetzt.

Termine

Bei Bedarf werden die Termine der Vorlesung und der Übung getauscht.

Vorlesung: Donnerstag, 13.15 - 14.45 Uhr in Raum IZ160

Übung: Mittwoch, 9.45 - 11.15 Uhr in Raum IZ160

Terminübersicht:

Wochentag Datum Typ Raum
Termine können sich noch ändern.
Mittwoch 23.10. Vorlesung IZ 160
Donnerstag 31.10. Vorlesung IZ 160
Mittwoch 6.11. Übung IZ 160
Donnerstag 7.11. Vorlesung IZ 160
Donnerstag 14.11. Vorlesung IZ 160
Mittwoch 20.11. Übung IZ 413a
Donnerstag 21.11. Vorlesung IZ 160
Mittwoch 27.11. Übung IZ 413a
Donnerstag 28.11. Vorlesung IZ 160
Mittwoch 4.12 Übung IZ 160
Donnerstag 5.12. Vorlesung IZ 160
Mittwoch 11.12 Übung IZ 413a
Donnerstag 12.12. Vorlesung IZ 160
Mittwoch 18.12. Übung IZ 413a
Donnerstag 9.1. Vorlesung IZ 160
Mittwoch 15.1. Vorlesung / Übung (kombiniert) IZ 160
Donnerstag 16.1. Vorlesung IZ 160
Mittwoch 22.1 Übung IZ 413a
Donnerstag 23.1. Vorlesung IZ 160
Donnerstag 30.1. Vorlesung IZ 160
Mittwoch 5.2 Übung IZ 413a
Donnerstag 6.2. Übung / Wiederholung IZ 160

Prüfung

Die Modulprüfung (30 Minuten mündliche Prüfung) findet nach der Vorlesungszeit des WS 2013/2014 statt. Termine für die mündlichen Prüfungen werden noch bekannt gegeben. Die Anmeldung erfolgt über das Prüfungsamt, die Terminvergabe über das Sekretariat des ISF.

Vorlesungsmaterialien

Die Vorlesungsunterlagen werden ausschließlich im Stud.IP hochgeladen. Bitte melden Sie sich daher dort frühzeitig für die Vorlesung an. In der Regel werden die Folien 2 Tage vor der Vorlesung bereit gestellt.

Literatur


  aktualisiert am 15.07.2013
TU_Icon_E_Mail_1_17x17_RGB Zum Seitenanfang