Home  | Legals | Sitemap | KIT

Formale Systeme

Formale Systeme
Type: Vorlesung / Übung (VÜ) Links:
Semester: WS 13/14
Time: 24.10.2013
14:00-15:30
30.22 Gaede


25.10.2013
11:30-13:00
30.22 Gaede

31.10.2013
14:00-15:30
30.22 Gaede

07.11.2013
14:00-15:30
30.22 Gaede

08.11.2013
11:30-13:00
30.22 Gaede

14.11.2013
14:00-15:30
30.22 Gaede

15.11.2013
11:30-13:00
30.22 Gaede

21.11.2013
14:00-15:30
30.22 Gaede

22.11.2013
11:30-13:00
30.22 Gaede

28.11.2013
14:00-15:30
30.22 Gaede

29.11.2013
11:30-13:00
30.22 Gaede

05.12.2013
14:00-15:30
30.22 Gaede

06.12.2013
11:30-13:00
30.22 Gaede

12.12.2013
14:00-15:30
30.22 Gaede

13.12.2013
11:30-13:00
30.22 Gaede

19.12.2013
14:00-15:30
30.22 Gaede

20.12.2013
11:30-13:00
30.22 Gaede

09.01.2014
14:00-15:30
30.22 Gaede

10.01.2014
11:30-13:00
30.22 Gaede

16.01.2014
14:00-15:30
30.22 Gaede

17.01.2014
11:30-13:00
30.22 Gaede

23.01.2014
14:00-15:30
30.22 Gaede

24.01.2014
11:30-13:00
30.22 Gaede

30.01.2014
14:00-15:30
30.22 Gaede

31.01.2014
11:30-13:00
30.22 Gaede

06.02.2014
14:00-15:30
30.22 Gaede

07.02.2014
11:30-13:00
30.22 Gaede

13.02.2014
14:00-15:30
30.22 Gaede

14.02.2014
11:30-13:00
30.22 Gaede

Lecturer: Prof.Dr. Peter Hans Schmitt
SWS: 4
LV-No.: 24086

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.