Logik und Formale Methoden

Kurzame
Logik u. Form. Methoden
Modulnummer
TI5002
Modulverantwortlicher
  • Berthold Franzen
Dozent
  • Berthold Franzen
  • Burkhardt Renz
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.

Qualifikations- und Lernziele

Die Teilnehmenden kennen grundlegende logische Konzepte und Begriffe, die sie zum praktischen Einsatz formaler Methoden bei der korrekten Modellierung sequentieller und nebenläufiger Systeme befähigen. Damit sind sie in der Lage, aus den zahlreichen Analysetechniken und Modellierungsansätzen diejenigen auszuwählen, welche geeignet sind, die interessierenden Systemeigenschaften anhand eines Modells zu analysieren.

Lerninhalte
  • 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
Moduldauer (Semester)
1
Unterrichtssprache
Deutsch
Gesamtaufwand
6 CrP; 180 Stunden, davon etwa 60 Stunden Präsenzzeit.
Semesterwochenstunden
4
Lernformen

Vorlesung 2 SWS, Übung 2 SWS

Geprüfte Leistung

Prüfungsvorleistungen: 2 anerkannte Hausübungen

Prüfungsleistung: Klausur

Bewertungsstandard

Bewertung der Prüfungsleistung nach § 9 der Prüfungsordnung (Teil l)

Häufigkeit des Angebots
Einmal im Jahr
Literatur
  • M. Huth, M. Ryan: Logic in Computer Science: Modelling and Reasoning about Systems Cambridge University Press
  • M. Ben-Ari: Mathematical Logic for Computer Science Springer
  • M. Schenker: Logikkalküle in der Informatik Springer Vieweg
  • B. Renz: Lösungen mit dem MNI Proposition Analyzer MPA Technischer Bericht Fachhochschule Gießen-Friedberg
  • D. Jackson: Software Abstractions: Logic, Language, and Analysis MIT Press
  • M. Ben-Ari: Principles of the Spin Model Checker Springer
Voraussetzungen
Keine
Voraussetzung für Module