Model-Checking
» Diese Veranstaltung wird auf deutsch gehalten.
Vorlesung im Wintersemester 2003/2004
Art | Termine/Ort | Beginn | Veranstalter |
---|---|---|---|
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
- SMV - http://www-2.cs.cmu.edu/~modelcheck/smv.html
(Windows User sollten sich auch das SMV Manual holen - bei der Source Code Version ist es bereits im Archiv enthalten) - SPIN - http://spinroot.com/spin/Src/
Weiterhin werden benötigt: Wird Spin unter Windows installiert, muss die Datei spin410.exe nach spin.exe umbenannt werden, ansonsten findet XSpin nicht die passende Datei. - UPPAAL2K - http://www.docs.uu.se/docs/rtmv/uppaal/download.html
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.