SE5009 Interaktives Spezifizieren und Verifizieren von Softwareartefakten

Modulverantwortliche
  • Prof. Dr. Burkhardt Renz
Lehrende
  • Prof. Dr. Burkhardt Renz
Notwendige Voraussetzungen zur Teilnahme

Keine

Empfohlene Voraussetzungen zur Teilnahme

TI5002 Logik und Formale Methoden

Kurzbeschreibung

Verständnis für die formale Spezifikation von Transitionssystemen; Formales Design von Softwareartefakten in der Sprache Alloy 6 und interaktives Arbeiten mit dem Alloy Analyzer; Model Finding und Model Checking

Inhalte
  • Formale Beschreibung von Softwaresystemen als Transitionssysteme
  • Spezifikation von Strukturen in der relationalen Logik von Alloy
  • Idiome der Spezifikation von Zustandsübergängen mit Alloy 6
  • Spezifikation von Algorithmen, Mustern und anderen Softwareartefakten als Transitionssysteme
  • Arbeiten mit dem Alloy Analyzer im Model Finding und Model Checking
Qualifikations- und Lernziele

Fachkompetenzen

  • Die Studierenden können die Konzepte der Spezifikation von Software mittels Transitionssysteme mit eigenen Worten wiedergeben und zielgerichtet auswählen.
  • Sie können diese Konzepte konkret in der Sprache Alloy formulieren und mit dem Alloy Analyzer überprüfen.
  • Sie können diese Kenntnisse für die Analyse von Softwareartefakten verwenden.

Methodenkompetenzen (fachlich & überfachlich)

  • Die Studierenden können komplexe Sachverhalte formal korrekt und verifizierbar beschreiben.

Sozialkompetenzen

  • Da die praktischen Teile des Kurses kollaborativ in Gruppen von Studierenden durchgeführt werden, sind die Studierenden in der Lage, kooperativ im Team zu arbeiten, da dies für die Softwareentwicklung eine wichtige Voraussetzung ist.

Selbstkompetenzen

  • Die Studierenden können den Wert logischen Denkens nicht nur in der Softwaretechnik, sondern in allen Lebenslagen einschätzen und anerkennen.
ECTS-Leistungspunkte (CrP)
  • 6 CrP
  • Arbeitsaufwand 180 Std.
  • Präsenzzeit 60 Std.
  • Selbststudium 120 Std.
Lehr- und Lernformen
  • 4 SWS
  • Seminaristischer Unterricht 4 SWS
Studiensemester
  • Informatik (M.Sc. 2022)
Dauer
1 Semester
Häufigkeit des Angebots
Einmal im Jahr
Unterrichtssprache
Deutsch
Bonuspunkte

Nein

Bonuspunkte werden gemäß § 9 (4) der Allgemeinen Bestimmungen vergeben. Art und Weise der Zusatzleistungen wird den Studierenden zu Veranstaltungsbeginn rechtzeitig und in geeigneter Art und Weise mitgeteilt.

Prüfungsleistungen

Prüfungsvorleistung: Keine

Prüfungsleistung: Projektarbeit oder mündliche Prüfung (Art des Leistungsnachweises wird den Studierenden rechtzeitig und in geeigneter Weise bekannt gegeben.)

Benotung
Die Bewertung des Moduls erfolgt gemäß §§ 9, ggf. 12 (Teilleistungen), ggf. 18 (Arbeiten, Kolloquien) der Allgemeinen Bestimmungen (Teil I der Prüfungsordnung).
Verwendbarkeit
Gemäß § 5 der Allgemeinen Bestimmungen (Teil I der Prüfungsordnung) Verwendbarkeit in allen Masterstudiengänge der THM möglich.
Literatur, Medien
  • Jackson, D.: Software Abstractions. MIT Press.
  • Lamport, L.: Specifying Systems. Addison Wesley.
  • Brunel, J.; Chemouil D.; Cunha, A.; Macedo, N.: Formal Software Design with Alloy 6. https://haslab.github.io/formal-software-design/index.html
  • Renz, B.: Erste Begegnung mit Alloy 6 sowie weitere Artikel zum Thema https://esb-dev.github.io/isv.html

Rechtliche Hinweise