Informationen zum Seminar
AVACS: Automatic Verification and Analysis of Complex Systems (SS 2003)
|
|
Verantwortlich
|
Prof. Dr. Bernd
Becker, Dipl.-Inf. Marc Herbstritt |
|
Termine
|
Vortragstermine:
- Freitag, 11.07.2003, 13:30-16:30 (Thema 1+2)
- Samstag, 12.07.2003, 9:00-12:00 (Thema 3+4)
Die Vorträge finden im Multimedia-Hörsaal
Geb. 051 Raum 00-031 statt.
|
2. Besprechungstermin: Donnerstag,
05. Juni 2003, 13:00 im Besprechungsraum des Lehrstuhls
(Geb. 051, Raum 01-031)
Topics: Definitive Terminfestlegung für die
Vorträge (Ende Juni, Anfang Juli)
|
1. Besprechungstermin: Donnerstag,
22. Juni 2003, 13:00 im Besprechungsraum des Lehrstuhls
(Geb. 051, Raum 01-031)
Topics: Genereller Stand der Dinge
|
Vorbesprechungstermin: Mittwoch,
30. April 2003, 15:00 im Besprechungsraum des Lehrstuhls
(Geb. 051, Raum 01-031)
Topics: Organisation, Einführung, Einteilung
|
|
|
Beschreibung
|
In diesem Seminar geht es um die formale Verifikation im Umfeld komplexer System wie z.B. System-on-Chip (SoC), eingebettete Systeme, hybride Systeme, ...
Das Seminar orientiert sich an:
Clarke, E.M.; Grumberg, O.; Peled, D.A.; "Model Checking", MIT Press,1999
|
|
Themenliste
|
Thema 1: Model Checking Einfuehrung
Relevante Kapitel: 3,4,5,6
Bearbeiter: Mariner, Christian; Staudenmaier, Armin
|
Thema 2: Equivalences and Preorders between Structures, Compositional Reasoning
Relevante Kapitel: 11,12
Bearbeiter: Degen, Markus; Wimmer, Ralf
|
Thema 3: Abstraction + Symmetry
Relevante Kapitel: 13,14
Bearbeiter: Drescher, Michael; Vossen, Anselm
|
Thema 4: Discrete Real Time, Continuous Real Time
Relevante Kapitel: 16,17
Bearbeiter: Eisinger, Jochen; Knapp, Markus
|
|
|
Ausarbeitung
|
Jeder Seminar-Teilnehmer hält gegen Ende des Semesters einen
20-25 Minuten Vortrag, der mittels eines Screen-Recording-Tools
aufgezeichnet wird. Ausserdem muss jeder Teilnehmer eine 15-30 seitige
schriftliche Ausarbeitung zu seinem Thema bis Ende September abgeben.
Kreditpunkte werden erst nach dem Vortrag und der Abgabe der Ausarbeitung
vergeben.
Alle Ausarbeitungen müssen in LaTeX geschrieben werden. Es sollte
einheitlich die Style-Vorlage der
LNCS (für Proceedings/Multi-Author Volumes) benutzt werden.
Das Style-File kann man hier downloaden: [llncs.cls].
Die Ausarbeitungen stehen gesammelt hier zur Verfügung: [AVACS Seminar Ausarbeitungen (PDF, ca. 1.3MB)]
|
|
Bewertung
|
Die Endbenotungen sind hier einsehbar: [AVACS Seminar Benotung]
|
|
Literatur
|
- Edmund M. Clarke ; Orna Grumberg ; Doron A. Peled: Model Checking. ISBN 0-262-03270-8. Frei 91: CI/6.0/2
- Kropf, Thomas: Introduction to Formal Hardware Verification. ISBN 3-540-65445-3. Frei 91: CB/6.3/19
- Folien zur Vorlesung VLSI-Entwurf von
Prof. Dr.-Ing. C. Scholl im WS2001/02: [folien]
- J.P. Katoen - Concepts, Algorithms, and Tools for Model
Checking (Vorlesungskript 1998/99) [download]
|