Mathematical Logic and Formal Methods

Modulnummer
TI5002
Modulverantwortliche
Berthold Franzen
Dozenten
  • Berthold Franzen
  • Burkhardt Renz
  • Kurzbeschreibung
    The module treats basic concepts, notions, methods and tools for the practical application of formal methods for correct modelling of sequential and concurrent systems.
    Qualifikations- und Lernziele

    The students know basic concepts and notions, which enable them to practically apply formal methods for correct modelling of sequential and concurrent systems. They are able to choose from numerous analysis techniques and modelling approaches those which are suited best to investigate relevant system properties by means of a model.

    Lerninhalte
    • Propositional logic: language, semantics, natural deduction, normal forms, decision questions, SAT solver, applications in software engineering with MPA (MNI Proposition Analyzer)
    • first order logic: language, semantics, natural deduction, decision problems, expressive power of fol, micro models of software with Alloy
    • Temporal logic: language of linear temporal logic (LTL), semantics, decision questions, model checking with Spin
    Moduldauer (Semester)
    1
    Unterrichtssprache
    Deutsch
    Gesamtaufwand
    6 CrP; 180 Stunden, davon etwa 60 Stunden Präsenzzeit.
    Semesterwochenstunden
    4
    Lernformen
    Lecture 2 sppw Exercises 2 sppw
    Geprüfte Leistung
    Written exam
    Bewertungsstandard
    according to examination regulations (§ 9)
    Häufigkeit des Angebots
    Yearly
    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
    None
    Voraussetzung für Module