Formale Systeme

  • Type:
  • Semester: WS 18/19
  • Time: 18.10.2018
    14:00 - 15:30 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau


    19.10.2018
    11:30 - 13:00 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    25.10.2018
    14:00 - 15:30 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    26.10.2018
    11:30 - 13:00 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    02.11.2018
    11:30 - 13:00 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    08.11.2018
    14:00 - 15:30 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    09.11.2018
    11:30 - 13:00 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    15.11.2018
    14:00 - 15:30 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    16.11.2018
    11:30 - 13:00 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    22.11.2018
    14:00 - 15:30 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    23.11.2018
    11:30 - 13:00 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    29.11.2018
    14:00 - 15:30 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    30.11.2018
    11:30 - 13:00 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    06.12.2018
    14:00 - 15:30 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    07.12.2018
    11:30 - 13:00 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    13.12.2018
    14:00 - 15:30 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    14.12.2018
    11:30 - 13:00 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    20.12.2018
    14:00 - 15:30 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    21.12.2018
    11:30 - 13:00 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    10.01.2019
    14:00 - 15:30 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    11.01.2019
    11:30 - 13:00 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    17.01.2019
    14:00 - 15:30 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    18.01.2019
    11:30 - 13:00 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    24.01.2019
    14:00 - 15:30 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    25.01.2019
    11:30 - 13:00 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    31.01.2019
    14:00 - 15:30 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    01.02.2019
    11:30 - 13:00 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    07.02.2019
    14:00 - 15:30 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau

    08.02.2019
    11:30 - 13:00 wöchentlich
    30.22 Gaede-Hörsaal
    30.22 Physik-Flachbau


  • Lecturer: Mattias Ulbrich
    Prof. Dr. Bernhard Beckert
  • SWS: 4
  • Lv-No.: 24086
Voraussetzungen

Die Voraussetzungen werden in der Modulbeschreibung erläutert.

Beschreibung

Diese Vorlesung soll die Studierenden einerseits in die Grundlagen der formalen Modellierung und Verifikation einführen und andererseits vermitteln, wie der Transfer von der Theorie zu einer praktisch einsetzbaren Methode betrieben werden kann.
Es wird unterschieden zwischen der Behandlung statischer und dynamischer Aspekte von Informatiksystemen.

  • Statische Modellierung und Verifikation
    Anknüpfend an Vorkenntnisse der Studierenden in der Aussagenlogik, werden Kalküle für die aussagenlogische Deduktion vorgestellt und Beweise für deren Korrektheit und Vollständigkeit besprochen. Es soll den Studierenden vermittelt werden, dass solche Kalküle zwar alle dasselbe Problem lösen, aber unterschiedliche Charakteristiken haben können. Beispiele solcher Kalküle können sein: der Resolutionskalkül. Tableaukalkül, Sequenzen- oder Hilbertkalkül. Weiterhin sollen Kalküle für Teilklassen der Aussagenlogik vorgestellt werden, z.B. für universelle Hornformeln.
    Die Brücke zwischen Theorie und Praxis soll geschlagen werden durch die Behandlung von Programmen zur Lösung aussagenlogischer Erfüllbarkeitsprobleme (SAT-solver).

    Aufbauend auf den aussagenlogischen Fall werden Syntax, Semantik der Prädikatenlogik eingeführt. Es werden zwei Kalküle behandelt, z.B. Resolutions-, Sequenzen-, Tableau- oder Hilbertkalkül. Wobei in einem Fall ein Beweis der Korrektheit und Vollständigkeit geführt wird.
    Die Brücke zwischen Theorie und Praxis soll geschlagen werden durch die Behandlung einer gängigen auf der Prädikatenlogik fußenden Spezifikationssprache, wie z.B. OCL, JML oder ähnliche. Zusätzlich kann auf automatische oder interaktive Beweise eingegangen werden.
  • Dynamische Modellierung und Verifikation
    Als Einstieg in Logiken zur Formalisierung von Eigenschaften dynamischer Systeme werden aussagenlogische Modallogiken betrachtet in Syntax und Semantik (Kripke Strukturen) jedoch ohne Berücksichtigung der Beweistheorie.
    Aufbauend auf dem den Studenten vertrauten Konzept endlicher Automaten werden omega-Automaten zur Modellierung nicht terminierender Prozesse eingeführt, z.B. Büchi Automaten oder Müller Automaten. Zu den dabei behandelten Themen gehören insbesondere die Abschlusseigenschaften von Büchi Automaten.
    Als Spezialisierung der modalen Logiken wird eine temporale modale Logik in Syntax und Semantik eingeführt, z.B. LTL oder CTL.
    Es wird der Zusammenhang hergestellt zwischen Verhaltensbeschreibungen durch omega-Automaten und durch Formeln temporalen Logiken.
    Die Brücke zwischen Theorie und Praxis soll geschlagen werden durch die Behandlung eines Modellprüfungsverfahrens (model checking).
Literaturhinweise

Vorlesungsskriptum 'Formale Systeme',
User manuals oder Bedienungsanleitungen der benutzten Werkzeuge (SAT-solver, Theorembeweiser, Modellprüfungsverfahren (model checker)).

Weiterführende Literatur

Wird in der Vorlesung bekannt gegeben.

Lehrinhalt

Diese Vorlesung soll die Studierenden einerseits in die Grundlagen der formalen Modellierung und Verifikation einführen und andererseits vermitteln, wie der Transfer von der Theorie zu einer praktisch einsetzbaren Methode betrieben werden kann.
Es wird unterschieden zwischen der Behandlung statischer und dynamischer Aspekte von Informatiksystemen.

  • Statische Modellierung und Verifikation
    Anknüpfend an Vorkenntnisse der Studierenden in der Aussagenlogik, werden Kalküle für die aussagenlogische Deduktion vorgestellt und Beweise für deren Korrektheit und Vollständigkeit besprochen. Es soll den Studierenden vermittelt werden, dass solche Kalküle zwar alle dasselbe Problem lösen, aber unterschiedliche Charakteristiken haben können. Beispiele solcher Kalküle können sein: der Resolutionskalkül. Tableaukalkül, Sequenzen- oder Hilbertkalkül. Weiterhin sollen Kalküle für Teilklassen der Aussagenlogik vorgestellt werden, z.B. für universelle Hornformeln.
    Die Brücke zwischen Theorie und Praxis soll geschlagen werden durch die Behandlung von Programmen zur Lösung aussagenlogischer Erfüllbarkeitsprobleme (SAT-solver).

    Aufbauend auf den aussagenlogischen Fall werden Syntax, Semantik der Prädikatenlogik eingeführt. Es werden zwei Kalküle behandelt, z.B. Resolutions-, Sequenzen-, Tableau- oder Hilbertkalkül. Wobei in einem Fall ein Beweis der Korrektheit und Vollständigkeit geführt wird.
    Die Brücke zwischen Theorie und Praxis soll geschlagen werden durch die Behandlung einer gängigen auf der Prädikatenlogik fußenden Spezifikationssprache, wie z.B. OCL, JML oder ähnliche. Zusätzlich kann auf automatische oder interaktive Beweise eingegangen werden.
  • Dynamische Modellierung und Verifikation
    Als Einstieg in Logiken zur Formalisierung von Eigenschaften dynamischer Systeme werden aussagenlogische Modallogiken betrachtet in Syntax und Semantik (Kripke Strukturen) jedoch ohne Berücksichtigung der Beweistheorie.
    Aufbauend auf dem den Studenten vertrauten Konzept endlicher Automaten werden omega-Automaten zur Modellierung nicht terminierender Prozesse eingeführt, z.B. Büchi Automaten oder Müller Automaten. Zu den dabei behandelten Themen gehören insbesondere die Abschlusseigenschaften von Büchi Automaten.
    Als Spezialisierung der modalen Logiken wird eine temporale modale Logik in Syntax und Semantik eingeführt, z.B. LTL oder CTL.
    Es wird der Zusammenhang hergestellt zwischen Verhaltensbeschreibungen durch omega-Automaten und durch Formeln temporalen Logiken.
    Die Brücke zwischen Theorie und Praxis soll geschlagen werden durch die Behandlung eines Modellprüfungsverfahrens (model checking).
Ziel

Der Studierende soll in die Grundbegriffe der formalen Modellierung und Verifikation von Informatiksystemen eingeführt werden.

Der Studierende soll die grundlegende Definitionen und ihre wechselseitigen Abhängigkeiten verstehen und anwenden lernen.

Der Studierende soll für kleine Beispiele eigenständige Lösungen von Spezifikationsaufgaben finden können, gegebenfalls mit Unterstützung entsprechender Softwarewerkzeuge.

Der Studierende soll für kleine Beispiele selbständig Verifikationsaufgaben lösen können, gegebenfalls mit Unterstützung entsprechender Softwarewerkzeuge.