Logik und Formale Methoden

Modulnummer
TI5002
Modulverantwortliche
Berthold Franzen
Dozenten
  • 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 Teilnehmer 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