13877 - Formale Methoden für die Softwaretechnik Modulübersicht

Modulnummer: 13877
Modultitel:Formale Methoden für die Softwaretechnik
  Formal Methods for Software Engineering
Einrichtung: Fakultät 1 - MINT - Mathematik, Informatik, Physik, Elektro- und Informationstechnik
Verantwortlich:
  • Prof. Dr. rer. nat. Lambers, Leen
Lehr- und Prüfungssprache:Deutsch
Dauer:1 Semester
Angebotsturnus: jedes Sommersemester ungerader Jahre
Leistungspunkte: 8
Lernziele:Nach erfolgreichem Abschluss des Moduls haben die Studierenden Überblickswissen über formale Methoden in der Softwaretechnik. Sie sind mit entsprechender Werkzeugunterstützung vertraut. Sie kennen wesentliche Anwendungsszenarien im Bereich der Qualitätssicherung in der Softwaretechnik .
Sie sind in der Lage, selbständig Fachwissen auf dem Gebiet der formalen Methoden für die Softwaretechnik zu erarbeiten und zu präsentieren.
Inhalte:Es gibt zahlreiche formale Methoden zur Modellierung, Analyse und Transformation verschiedener Arten von Software-Artefakten (z.B. Anforderungsspezifikationen, Software-Designs, Laufzeitmodelle, Code, etc.). Der Einsatz formaler Methoden unterstützt die Einführung von mehr Genauigkeit und tieferem Verständnis dieser Software-Artefakte mit dem übergeordneten Ziel der Konstruktion qualitativ hochwertigerer Software-Systeme.

Einige der formalen Methoden konzentrieren sich auf zustandsbasiertes Verhalten (z. B. Automaten, Zustandsdiagramme oder Zustandsübergangssysteme), andere Methoden konzentrieren sich eher auf die Struktur (z. B. relationale Logik), oder auf die Kombination von beidem (z.B. Graphentransformation), was es erlaubt das Zusammenspiel von Struktur und Verhalten zu untersuchen.

Diese Vorlesung gibt einen Überblick über formale Methoden für die Softwaretechnik und die dazugehörige Werkzeugunterstützung. Die Anwendungsszenarien befassen sich mit verschiedenen Qualitätsaspekten eines Softwaresystems wie Safety, Security, Performance, Traceability, Adaptivität, etc. Ethische und gesellschaftliche Aspekte in Verbindung mit dem Einsatz von formalen Methoden in der Softwaretechnik werden thematisiert.
Empfohlene Voraussetzungen:Kenntnisse in
  • Grundlagen der Softwaretechnik
  • Grundlagen der Mathematik (Logik, Algebra)
  • Grundlagen der theoretischen Informatik (Berechenbarkeitstheorie und formale Sprachen)
z.B. Kenntnis des Stoffes der Module
  • 12104 Entwicklung von Softwaresystemen
  • 11787 Theoretische Informatik
  • 11112 Mathematik IT-1 (Diskrete Mathematik)
Zwingende Voraussetzungen:keine
Lehrformen und Arbeitsumfang:
  • Vorlesung / 2 SWS
  • Übung / 2 SWS
  • Seminar / 2 SWS
  • Selbststudium / 150 Stunden
Unterrichtsmaterialien und Literaturhinweise:
  • Principles of Model Checking, Christel Baier and Joost-Pieter Katoen, MIT Press 2008
  • Software Abstractions - Logic, Language, and Analysis, Daniel Jackson, MIT Press 2006
  • Graph Transformation for Software Engineers, Reiko Heckel and Gabriele Taentzer, Springer, 2020
Weitere Literatur wird zu Semesterbeginn angegeben.
Modulprüfung:Voraussetzung + Modulabschlussprüfung (MAP)
Prüfungsleistung/en für Modulprüfung:Voraussetzung für die Modulabschlussprüfung:
  • Erfolgreiche Bearbeitung und Präsentation von Übungsaufgaben (60 Stunden) sowie erfolgreiche Ausarbeitung und 30-minütiger Präsentation eines ausgewählten Seminarthemas (40 Stunden)
Modulabschlussprüfung:
  • Klausur, 90 min. ODER
  • mündliche Prüfung, 30-45 min. (bei geringer Teilnehmerzahl)
In der ersten Lehrveranstaltung wird bekanntgegeben, ob die Prüfungsleistung in schriftlicher oder mündlicher Form zu erbringen ist.
Bewertung der Modulprüfung:Prüfungsleistung - benotet
Teilnehmerbeschränkung:keine
Zuordnung zu Studiengängen:
  • Master (universitär) / Informatik / PO 2008
Bemerkungen:
  • Studiengang Informatik M.Sc.: Wahlpflichtmodul in Komplex „Grundlagen der Informatik“ (Niveaustufe 400)
Veranstaltungen zum Modul:
  • Vorlesung: Formale Methoden für die Softwaretechnik
  • Übung zur Vorlesung
  • Seminar zur Vorlesung
  • Zugehörige Prüfung
Veranstaltungen im aktuellen Semester:
  • keine Zuordnung vorhanden