Hauptinhalt

Formale Methoden in der Softwaretechnik

Formale Methoden werden zur formalen Spezifikation und Analyse von Softwaresystemen verwendet sowie als geeigneten Abstraktionsebene für die Beschreibung und Lösung von softwaretechnischen Problemen. Ausgehend von endlichen Automaten beginnen wir mit der formalen Spezifikation von einfachen Systemen und analysieren diese mit Model-Checking-Verfahren. Zur Spezifikation und Analyse von realistischeren Systemen verfeinern wir die Zustandsspezifikation durch Datenstrukturen. Graphen können flexibel zur Spezifikation von Datenstrukturen eingesetzt werden. Ihre Änderungen können mit Graphtransformationen systematisch definiert werden. Auf dieser Basis lassen sich typische Aktivitäten der Softwareentwicklung, wie z.B. der Systementwurf und das Testen von Programmen, formal spezifizieren und analysieren. Daneben betrachten wir einfache Programmverifikation. Abschließend widmen wir uns einem ausgewählten Problem der Softwaretechnik und entwickeln gemeinsam eine Spezifikations- und Analysetechnik für dieses Problem.

Qualifikationsziele

Nach der Beendigung dieses Moduls werden die Studierenden

in der Lage sein, Systeme, Systemeigenschaften und Softwareentwicklungsaktivitäten zu formalisieren,
wissen, wie Systemeigenschaften automatisch analysiert und verifiziert werden können,
eher in der Lage sein, die Stärken und Schwächen formaler Methoden in der Softwaretechnik zu beurteilen,
wissenschaftlicher Arbeitsweisen (Erkennen, Formulieren, Lösen von Problemen, Schulung des Abstraktionsvermögens) geübt haben und
die mündlichen Kommunikationsfähigkeit durch Einüben der freien Rede vor einem Publikum und bei der Diskussion trainiert haben.

Organisatorisches

Lehrveranstaltende: Prof. Taentzer
Vorlesungs- und Klausurtermine unter Modulnummer: LV-12-079-200
Übungstermine unter Modulnummer: LV-12-079-201
SWS: 4+2, Leistungspunkte: 9

Voraussetzungen: Keine. Empfohlen werden die Kompetenzen, die in den Modulen Theoretische Informatik, Logik und Softwaretechnik vermittelt werden.

Leistungen: Erreichen von mindestens 50 Prozent der Punkte aus den wöchentlich zu bearbeitenden Übungsaufgaben und mündliche Präsentation der Lösung von mindestens zwei der Übungsaufgaben. Mündliche Prüfung oder Klausur.

Weitere Hinweise: Aktuelle Informationen und Ankündigungen zur Vorlesung werden grundsätzlich in der zugehörigen Ilias-Gruppe veröffentlicht. Sie können den Ordner Softwaretechnik in Ilias nutzen, um von dort aus zum aktuellen Semester und der zur Veranstaltung passenden Gruppe zu navigieren.

Literatur

H. Balzert: Lehrbuch der Software-Technik - Software-Entwicklung, 2. Aufl., Spektrum Akademischer Verlag 2000
C. Baier, J. Katoen: Principles of Model Checking, MIT Press 2008