=== 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 ===

• 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 ===

• Die Übung findet donnerstags 10:00 - 11:30 statt.
• Voraussichtliche Termine:
  • 19.04.2007
  • 03.05.2007
  • 24.05.2007
  • 14.06.2007 (Raum 2323, Lehrstuhl für Informatik 11)
  • 28.06.2007 (Raum 2323, Lehrstuhl für Informatik 11)

=== Ü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
• Bastian Schlich
• Allgemeine Fragen werden im Forum beantwortet.