Home | english  | Impressum | Sitemap | KIT

Formale Systeme

Formale Systeme
Typ: Vorlesung / Übung (VÜ)
Semester: WS 11/12
Ort:

30.22 Gaede

Zeit:

Do, 14:00-15:30
Fr, 11:30-13:00

Beginn: 20.10.2011
Dozent:

Prof. Dr. Peter H. Schmitt

David Farago
Christoph Scheben
Mattias Ulbrich

SWS: 4
LVNr.: <a target="lvn" href="https://studium.kit.edu/meineuniversitaet/Seiten/vorlesungsverzeichnis.aspx?page=event.asp&objgguid=NEW&gguid=0x54c8b640e463224a83897d2b86e4b8c1">24086</a>

Hier geht es zur Vorlesung Formale Systeme im WS 2014/15.

Webseite der Vorlesung

Auf der Webseite zur Vorlesung finden Sie aktuelle Ankündigungen, die Materialien und den Login.

Vortragssprache:

Deutsch

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:

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.