TU BRAUNSCHWEIG

Fundamente des Software Engineering (FSE)

Aktuelles

  • Am Montag, den 16.7., findet von 9:45h - 11:15h in IZ 413a die 8. Übung statt.
  • Am Donnerstag, den 19.7., beginnt um 13:15h die letzte Übungs(Frage-)stunde in Raum IZ 161.

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: Donnerstags, 13:15h - 14:45h, IZ 161

  • Vorlesungstermine: 12.4., 19.4., 23.4. (Montag, 09:45 - 11:15, IZ 358), 3.5., 14.5. (Montag, 09:45 - 11:15, IZ 358), 24.5., 4.6. (Montag, 09:45 - 11:15, IZ 358), 14.6., 21.6., 25.6. (Montag, 09:45 - 11:15, IZ 358), 28.6., 2.7. (Montag, 09:45 - 11:15, IZ 358), 5.7., 12.7.

Übung: Montags, 09:45h - 11:15h, IZ 358

  • Übungstermine: 26.4., 7.5., 21.5. (IZ413a), 7.6. (Donnerstag, 13:15 - 14:45, IZ 161), 11.6. (IZ413a), 25.6., 9.7. (IZ413a), 16.7. (IZ413a), 19.7. (Donnerstag, 13:15 - 14:45, IZ 161)

Mailingliste

Für aktuelle Informationen zur Lehrveranstaltung ist eine Mailingliste eingerichtet. Bitte tragen Sie sich unter http://listserv.tu-bs.de/archives/fse12.html in die Mailingliste ein.

Prüfung

Die Modulprüfung (30 Minuten mündliche Prüfung) findet nach der Vorlesungszeit des SS 2012 statt. Termine für die mndlichen Prüfungen sind am 26. Juli und am 10. und 11. September. Die Anmeldung erfolgt über das Prüfungsamt, die Terminvergabe über das Sekretariat des SSE.

Vorlesungsmaterialien

Hier werden Sie die Vorlesungsfolien zum Download (aus der TUBS Domain) finden. In der Regel werden die Folien 2 Tage vor der Vorlesung bereit gestellt.

Übungen

Zu jeder Übung gibt es ein Übungsblatt, das Sie zur Vorbereitung der Übung als Hausaufgabe bearbeiten. In der Übung werden die Lösungen der Aufgaben besprochen. Eine Pflichtabgabe von Übungsaufgaben gibt es nicht. Es wird jedoch empfohlen, Ihre Lösungen zu Ihrer eigenen Kontrolle abzugeben und korrigieren zu lassen. Eine Sammlung an Links der verwendeten Tools finden Sie hier.

Übungsblätter

Literatur


  aktualisiert am 15.01.2013
TU_Icon_E_Mail_1_17x17_RGB Zum Seitenanfang