|
Model-Checking
|
|
V2+Ü1: Vorlesung mit Übungen im Hauptstudium
|
|
Veranstalter
|
| Name der Universität |
RWTH Aachen |
| Anbietende Einrichtung |
Lehrstuhl für Informatik VII |
| Dozent / Dozentin |
Prof. Dr. Wolfgang Thomas |
| Anschrift |
Ahornstr. 55
D-52056 Aachen
|
|
|
Anmeldung
|
|
13.10.2003
|
|
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 mehreren
Ansätzen 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
|
|
Notwendige Vorkenntnisse
|
|
Die Grundlagen der Automatentheorie, wie sie im Grundstudium
vermittelt werden, sind für die Teilnahme erforderlich.
|
|
Curriculare Einordnung beim Anbieter
|
|
Theorievorlesung im Hauptstudium. Die Vorlesung wird alle 2
bis 3 Semester an der RWTH Aachen angeboten.
|
|
Ablauf
|
|
Die Vorlesung wird mit einem Screen Recording Tool
aufgezeichnet und kann dann als Videodatei heruntergeladen
werden.
|
|
Prüfungsbedingungen
|
|
Wer die Klausur (90 Minuten) besteht, erhält einen
Übungsschein.
|
|
Umfang
|
|
|
|
Betreuung
|
| Name des Betreuers / der Betreuerin |
Philipp Rohde |
| Adresse |
Lehrstuhl für Informatik VII,
RWTH Aachen |
| Telefon |
(0241) -80 -21716 |
| E-Mail |
rohde@informatik.rwth-aachen.de |
| Sprechstunden |
Montag, 14.00-15.00 Uhr |
|
|
Startseite
|
|
http://www-i7.informatik.rwth-aachen.de/d/teaching/ws0304/modelchk/
|
