| | Matrikelnummer
=== Inhalt ===
Anwendung formaler Methoden in der Entwicklung eingebetteter Systeme:
formale Modelle,
hybride Systeme,
Verifikation,
Model Checking.
Die Vorlesung wird in Deutsch gehalten.
=== Literatur ===
D. Peled: Software Reliability Methods. Springer, 2001.
E. Clarke, O. Grumberg, D. Peled: Modelchecking. MIT Press, 2001.
B. Berard, M. Bidoit, A. Finkel: Systems and Software Verification. Springer, 2001
W. Ehrenberger: Software-Verifikation. Hanser, 2002.
=== Folien ===
| | Datum |
| Thema |
| Dokumente |
| | 10.04.2007 |
| Einführung |
| pdf |
| | 17.04.2007 |
| Signale und Systeme |
| pdf |
| | 24.04.2007 |
| Temporale Logiken |
| pdf1, pdf2 |
| | 15.05.2007 |
| CTL Model-Checking |
| pdf |
| | 22.05.2007 |
| Symbolic Model-Checking |
| pdf |
| | 05.06. & 12.06.2007 |
| Timed Automata |
| pdf |
| | 19.06.2007 |
| Hybride Systeme 1 |
| pdf1, pdf2 |
| | 26.06.2007 |
| [mc]square |
| pdf |
| | 03.07.2007 |
| Hybride Systeme 2 |
| pdf |
=== Errata ===
Temporale Logiken S. 7 oben, 4. Beispiel: Die Formel cUd ist auch im letzten Knoten wahr.
CTL Model-Checking S. 3 a)-f): Die Teilformeln werden für alle Zustände in der Kripke-Struktur überprüft, nicht nur für x0.
=== Mitschrift ===
Mitschrift der Vorlesung erstellt von Herrn Matthias Lebok (Student). Die Mitschrift wird ohne jegliche Gewähr angeboten. Wer Fehler findet, kann diese im Forum melden (pdf).
Errata: Am Ende des Semesters wird eine korrigierte Version zur Verfügung gestellt.
=== Übung ===
=== Übungsschein ===
Um den Übungsschein zu erwerben
dürfen Sie maximal einen Übungstermin mit Attest entschuldigt versäumen,
müssen Sie mindestens einmal mit Ihrer Gruppe eine Lösung präsentieren
und müssen die Klausur bestehen (voraussichtlich 10.07.2007 10:00-11:00).
=== Kontakt ===
Gerlind Herberich
-
Allgemeine Fragen werden im Forum beantwortet.
|