TI5002 Logik und Formale Methoden

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

Das Modul behandelt Grundkonzepte, Begriffe, Methoden und Werkzeuge, mit denen formale Methoden praktisch eingesetzt werden können, um sequentielle und nebenläufige Systeme korrekt zu modellieren.

Inhalte
  • Aussagenlogik: Sprache, Semantik, Natürliches Schließen, Normalformen, Entscheidbarkeitsfragen der Aussagenlogik, SAT-Solver, Anwendungen in der Softwaretechnik mit LWB (Logic WorkBench)
  • Prädikatenlogik: Sprache, Semantik, Natürliches Schließen, Normalformen, Unentscheidbarkeit der Prädikatenlogik, Ausdruckskraft der Prädikatenlogik, Mikromodelle von Software mit Alloy
  • Temporale Logik: Sprache der linearen temporalen Logik (LTL), Semantik, Entscheidbarkeitsfragen, Model Checking mit Spin
Qualifikations- und Lernziele

Fachkompetenzen

  • Die Studierenden können grundlegende logische Konzepte und Begriffe erklären und einschätzen.

Methodenkompetenzen (fachlich & überfachlich)

  • Die Studierenden können formale Methoden praktisch einsetzen bei der korrekten Modellierung sequentieller und nebenläufiger Systeme.
  • Sie können aus den erlernten Analysetechniken und Modellierungsansätzen diejenigen auswählen, welche geeignet sind, die für eine Anwendung interessierenden Systemeigenschaften anhand eines Modells zu verifizieren.

Sozialkompetenzen

  • Die Studierenden können die Möglichkeiten und Grenzen der vorgestellten Ansätze und Werkzeuge im Team diskutieren.
  • Sie können Andere von der Eignung eines gewählten Ansatzes zur Modellierung eines Systems überzeugen.

Selbstkompetenzen

  • Die Studierenden können sich eigenständig neuere Entwicklungen zum Einsatz formaler Methoden erarbeiten und ihre Anwendbarkeit für eine gegebene Aufgabe einordnen.
ECTS-Leistungspunkte (CrP)
  • 6 CrP
  • Arbeitsaufwand 180 Std.
  • Präsenzzeit 60 Std.
  • Selbststudium 120 Std.
Lehr- und Lernformen
  • 4 SWS
  • Vorlesung 2 SWS
  • Übung 2 SWS
Studiensemester
  • Informatik (M.Sc. 2010)
  • Ingenieur-Informatik (M.Sc. 2017)
  • Medizinische Informatik (M.Sc. 2014) - 1. - 2. Semester
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üfungsvorleistungen: Hausübungen (Anzahl der Hausübungen wird den Studierenden rechtzeitig und in geeigneter Weise bekannt gegeben.)

Prüfungsleistung: Klausur

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
  • Huth, M.; Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press.
  • Ben-Ari, M.: Mathematical Logic for Computer Science. Springer.
  • Schenker, M.: Logikkalküle in der Informatik. Springer Vieweg.
  • Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press.
  • Ben-Ari, M.: Principles of the Spin Model Checker. Springer.
  • Renz, B.: lwb Logic WorkBench. https://github.com/esb-lwb/lwb/wiki .

Rechtliche Hinweise