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).

Lernziele:

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.

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.