TU BRAUNSCHWEIG

Fundamente des Software Engineering (FSE)

Aktuelles

  • Die nächste Vorlesungen sind ist am Mittwoch, den 13.Juli, von 09:45h - 11:15h, in IZ 160.
  • Die nächste Übung ist am Donnerstag, den 7. Juli, von 13:15 - 14:45, in IZ 160. 
  •  Am Mittwoch, den 20. Juli, findet von 15:00h - 16:30h in IZ 160 ein Treffen zur Wiederholung und Prüfungsvorbereitung statt.

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 Spezifikaitonen für die Programme formal zu verifizieren.  Die Vorlesung behandelt folgende Themen:

  • Java Modeling Language (JML)
  • Formale Semantic 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 160

  • Achtung: Die erste Vorlesung ist am Mittwoch, 6. April, 09:45h - 11:15h.
  • Vorlesungstermine: 6.4. (Mi), 14.4., 21.4., 28.4., 5.5., 12.5.,19.5. (entfällt!), 26.5., 1.6. (Mi), 9.6., 23.6., 29.6. (Mi neu!), 30.6., 6.7. (Mi), 13.7. (Mi)

Übung: Mittwochs (14-tägig), 09:45h - 11:15h, IZ 160

  • Erste Übung: Mittwoch, 20. April, 09:45h - 11:15h, IZ 160
  • Übungstermine: 20.4., 4.5., 18.5., 8.6., 22.6., 7.7. (Do), 14.7. (Do, Raum 251)

Mailingliste

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

Prüfung

Die Modulprüfung (30 Minuten mündliche Prüfung) findet nach der Vorlesungszeit des SS 2011 im August/September statt. Termine für die mündlichen Prüfungen sind am 17. und 18. August und am 13. und 14. 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.

Literatur


  aktualisiert am 19.01.2012
TU_Icon_E_Mail_1_17x17_RGB Zum Seitenanfang