Model-Checking

» Diese Veranstaltung wird auf deutsch gehalten.

Vorlesung im Wintersemester 2003/2004

ArtTermine/OrtBeginnVeranstalter
V2 Mo 15:00 - 16:30 AH V 20.10.2003 Thomas, Löding
Ü1 Mi 17:00 - 17:45 AH II 12.10.2003 Rohde, Wallmeier

Inhalt

Model-Checking ist eine Methode zum automatischen Debugging und zur Verifikation von Software und Hardware. Es gehört heute zur industriellen Praxis (vor allem im Hardware-Entwurf und der Protokoll-Verifikation).

In diesem Kurs geben wir eine Einführung in mehrere Ansätze und erläutern sie durch Beispiele mit verschiedenen verfügbaren Software-Tools:

  • CTL-Model-Checking und das Tool SMV
  • LTL-Model-Checking und das Tool Spin
  • Verifikation von Realzeit-Eigenschaften und das Tool Uppaal

Model Checking Tools zum Praktikum

Typ

Es gibt eine einstündige Übung und ein ergänzendes Praktikum, das zweistündig ca. alle zwei Wochen stattfindet und in dem Aufgaben zu den vorgestellten Tools bearbeitet werden. Die Teilnahme am Praktikum ist freiwillig und das Praktikum ist nicht prüfungsrelevant.

Nur für Studierende der RWTH Aachen: Die Vorlesung kann \mit der Vorlesung "Automata on infinite objects" zu einem Kursus von 4 Stunden pro Woche kombiniert werden (V4 + Ü2). Die Übungen für die beiden Vorlesungen werden aufeinanderfolgend angeboten. Bei erfolgreichem Bestehen beider Kurse (Übungen und Klausur) kann man einen "großen Übungsschein" (V4 + Ü2) erhalten.

Die Vorlesung wird mit einem Screen Recording Tool aufgezeichnet, anschließend multimedial aufbereitet und sowohl hier auf diesen Seiten als auch später auf CD-ROM zur Verfügung gestellt.

Der Kurs wird als virtuelle Lehrveranstaltung im Rahmen von ULI - Universitärer Lehrverbund Informatik angeboten.

Anmeldung

Studierende der RWTH Aachen können sich wie üblich in der ersten Übung (Mi, 22.10.) für die Übungsgruppe in eine Liste eintragen.

Neben den Übungsplätzen für Studierende der RWTH Aachen gibt es weitere 20 Plätze für externe Übungsteilnehmer, die bei erfolgreicher Teilnahme einen Leistungsnachweis erhalten können. Die externen Teilnehmer können ihre Lösungen der Übungen in elektronischer Form einreichen und werden via Internet und E-Mail betreut.

Die Anmeldung für Externe erfolgt auf der ULI-Homepage www.uli-campus.de. Der Anmeldeschluß für Externe ist der 20. Oktober 2003.

Notwendige Vorkenntnisse

Die Grundlagen der Automatentheorie, wie sie im Grundstudium vermittelt werden, sind für die Teilnahme erforderlich.

Studienrelevanz

Der durch das erfolgreiche Bestehen der Klausur (90 Minuten) erworbene Schein wird an der RWTH Aachen als Studienleistung ("kleiner Übungsschein", V2 + Ü1) anerkannt. Als Externer informieren Sie sich bitte bei Ihrem zuständigen Prüfungsamt, ob der Schein bzw. die Credit Points an Ihrer Universität anerkannt werden.

Credit Points

4 ECTS