Modulbeschreibung

Modul: Modellprüfung - Beweiser und Algorithmen

Lehrveranstaltungen:

TitelTypSWSZeitraum
Modellprüfung - Beweiser und AlgorithmenVorlesung2Sommersemester
Modellprüfung - Beweiser und AlgorithmenGruppenübung2Sommersemester

Modulverantwortlich:

Prof. Görschwin Fey

Zulassungsvoraussetzungen:

Keine

Empfohlene Vorkenntnisse:

Grundlegende Kenntnisse zu Datenstrukturen und Algorithmen

Modulziele / angestrebte Lernergebnisse:

Fachkompetenz

Wissen

Studierende kennen

  • Algorithmen und Datenstrukturen für die Modellprüfung,
  • grundlegende Beweisverfahren sowie
  • den Einfluss der Modellierung und Spezifikation auf den Rechenaufwand für den Nachweis mittels Modellprüfung.
Fertigkeiten

Studierende können

  • Algorithmen und Datenstrukturen zur Modellprüfung erläutern und implementieren
  • abschätzen, ob sich eine Problemstellung mittels Boolescher Beweisverfahren oder Modellprüfung beantworten lässt, und
  • solche Lösungsverfahren realisieren.

Personale Kompetenzen

Sozialkompetenz

Studierende können

  • die jeweiligen Konzepte diskutieren und erläutern sowie
  • die Lösungen mündlich darstellen.
Selbstständigkeit

Studierende erlernen mittels Zusatzmaterial selbständig vertiefende Zusammenhänge der Konzepte aus der Vorlesung und erweiterte Lösungsverfahren.

Leistungspunkte Modul:

6 LP

Studienleistung:

Mündliche Prüfung

Arbeitsaufwand in Stunden:

Eigenstudium: 124, Präsenzstudium: 56


Lehrveranstaltung: Modellprüfung - Beweiser und Algorithmen

Dozent:

Görschwin Fey

Sprache:

Deutsch & Englisch

Zeitraum:

Sommersemester

Inhalt:

Correctness is a major concern in embedded systems. Model checking can fully automatically proof formal properties about digital hardware or software. Such properties are given in temporal logic, e.g., to prove "No two orthogonal traffic lights will ever be green."

And how do the underlying reasoning algorithms work so effectively in practice despite a computational complexity of NP hardness and beyond?

But what are the limitations of model checking?
How are the models generated from a given design?
The lecture will answer these questions. Open source tools will be used to gather a practical experience.

Among other topics, the lecture will consider the following topics:

  • Modelling digital Hardware, Software, and Cyber Physical Systems

  • Data structures, decision procedures and proof engines

    • Binary Decision Diagrams

    • And-Inverter-Graphs

    • Boolean Satisfiability

    • Satisfiability Modulo Theories

  • Specification Languages

    • CTL

    • LTL

    • System Verilog Assertions

  • Algorithms for

    • Reachability Analysis

    • Symbolic CTL Checking

    • Bounded LTL-Model Checking

    • Optimizations, e.g., induction, abstraction

  • Quality assurance

Literatur:

Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. 1999. Model Checking. MIT Press, Cambridge, MA, USA.

A. Biere, A. Biere, M. Heule, H. van Maaren, and T. Walsh. 2009. Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications. IOS Press, Amsterdam, The Netherlands, The Netherlands.

Selected research papers