Beschreibung:
Model Checking bezeichnet eine vollautomatisierbare
Verifikationstechnik für Hard- und Softwaresysteme. Die
zugrundeliegenden Algorithmen basieren im wesentlichen auf
Graphalgorithmen und Konzepten formaler Sprachen. Eine naive Umsetzung
der Algorithmen scheitert jedoch an dem Problem der Zustandsexplosion.
Um Systeme mit sehr großen oder unendlichem Zustandsraum behandeln
zu können, wurden in der Literatur verschiedene Strategien
vorgestellt. Das Seminar beschäftigt sich u.a. mit Ansätzen, die
dem Phänomen der Zustandsexplosion entgegenwirken können und die
es erlauben, Systeme mit unendlichem Zustandsraum zu behandeln.
U.a. werden Methoden zur Analyse von Echtzeitsystemen,
Konstruktionsverfahren des Quotientenraums unter
(Bi-)simulationsäquivalenz, randomisierte Speichertechniken und
Minimierungsalgorithmen für 
-Automaten behandelt.
Voraussetzungen: Das Seminar baut auf der im SS2003 gehaltenen Vorlesung Model Checking auf.
Bereich: A (alte und neue DPO).
Nachfolge-/Begleitveranstaltungen: Es besteht die Möglichkeit, parallel zum Seminar an einem Praktikum zum Thema ,,Model Checking`` teilzunehmen. Alternativ können Sie ein Praktikum zum Thema ,,Binäre Entscheidungsgraphen`` absolvieren. Die Teilnahme am Praktikum zum Thema ,,Binäre Entscheidungsgraphen`` ist unabhängig von der Teilnahme am Seminar. Dieses Praktikum richtet sich an alle Informatik-Studierende im Hauptstudium und setzt keinerlei Vorkenntnisse über Binäre Entscheidungsgraphen (oder Model Checking) voraus.
Termin: voraussichtlich Do, 16-18 Uhr, N1001
Vorbesprechung:
Eine erste Vorbesprechung für das
Seminar (und zugehöriges Praktikum zum Thema ,,Model Checking`` )
findet am Mittwoch, den 30.7.2003 in Hörsaal C im letzten
Teil der Vorlesung statt.
Interessierte,
die an diesem Termin verhindert sind,
bitten wir, sich möglichst bis zum 29.7.2003 mit den Veranstaltern in
Verbindung zu setzen (Email: Frank Ciesinski
ciesinsk@cs.uni-bonn.de
).
Interessierte am Praktikum zum Thema ,,Binäre Entscheidungsgraphen``
melden sich bitte ebenfalls per email über die o.g. Adresse.
Teilnehmer: Es liegt noch keine Teilnehmerliste vor.
Teilnehmerinnen und Teilnehmer beachten bitte auch folgendes Handout, welches die Details der Ausarbeitung, des Vortrages und der Vorbesprechungen beinhaltet.