Willkommen auf der Webseite zum Seminar 1917 Model Checking im Sommersemester 2014!

Auf dieser Seite finden Sie alle wichtigen Informationen zum Seminar. Besuchen Sie daher bitte regelmäßig diese Seite.

Inhalt

Der Begriff "Model Checking" wirkt auf den ersten Blick etwas missverständlich, besonders wenn er auf Modelle (z.B. von Software) angewandt wird.
Das Wort "Model" in "Model Checking" bezieht sich auf den Modellbegriff in formaler Logik. Ein logischer Ausdruck kann zu "wahr" oder "falsch" interpretiert werden, je nachdem auf welches Objekt (in einem sehr allgemeinen Sinne) er angewandt wird. Modelle eines logischen Ausdrucks sind die Objekte, für die der Ausdruck zu wahr ausgewertet wird.

Model Checking bedeutet daher, einen logischen Ausdruck auf Gültigkeit zu überprüfen. Im Kontext der Modellverifikation unterscheidet sich Model Checking von anderen Verifikationsverfahren dadurch, dass hier eine Spezifikation (die logische Formel) zusammen mit einem Modell (dem Objekt) automatisch daraufhin überprüft wird, ob das Modell die Spezifikation erfüllt. Spezifikationen werden in diesem Zusammenhang meist in Temporalen Logiken (z.B. LTL, CTL) formuliert, als Modelle kommen u.a. Transitionssysteme und Petrinetze in Frage. Wird eine Spezifikation erfüllt, so gibt der Model Checker "ja" aus, wird sie nicht erfüllt, so wird ein Gegenbeispiel ausgegeben. Dies kann zum Beispiel ein Ablauf eines Petrinetzes sein, in dem die Verletzung der Spezifikation deutlich wird.

Zeitplan (Änderung!)

Durchführung

In diesem Seminar werden Arbeiten vorgestellt, die aufeinander aufbauen. Zudem wird vorab ein Basistext zur Verfügung gestellt, den alle Teilnehmer gelesen und verstanden haben müssen.

Themen

Um die Verteilung der Themen einzusehen und für den Download der jeweiligen Papiere sehen Sie bitte hier nach.

Für Mitteilungen an den Verantwortlichen an der Fernuni steht für individuelle Fragen das Kurspostfach kurs1917@fernuni-hagen.de zur Verfügung.