Materialien
Vorlesungsmaterial
Leistungsnachweis
Prüfungskriterien Verifikation probabilistischer Systeme - Sommersemester 2013
Übersicht
| Beschreibung |
Eingebettete Systeme besitzen eine digitale Steuerung, interagieren in der Regel aber mit kontinuierlichen physikalischen Größen wie Temperatur, Geschwindigkeit und Zeit. Über die reine Frage nach der (funktionalen) Korrektheit hinaus sind oft Informationen wie die erwartete Lebensdauer, der mittlere Durchsatz oder die Zuverlässigkeit eines Systems von großem Interesse. Dazu müssen Effekte berücksichtigt werden, die stochastischer Natur sind (z. B. Kommunikation über unzuverlässige Kanäle, endliche Lebensdauer von Komponenten ...). Um diese untersuchen zu können, müssen Modelle entwickelt werden, die es erlauben, mathematisch präzise stochastische Effekte zu modellieren. Die in der Vorlesung vorgestellten Modelle sind Markow-Ketten mit diskreter und kontinuierlicher Zeit. Sie haben den Vorteil, dass es für eine ganze Reihe von interessanten Maßen effiziente Algorithmen gibt. Wir betrachten Markow-Ketten aus der Perspektive der Informatik mit dem Schwerpunkt auf Algorithmen zu ihrer Analyse. Die notwendigen Grundlagen, die über die Mathematik-Vorlesungen für ESE/Informatik im Bachelorstudium und die Vorlesung "Technische Informatik" hinausgehen, werden in der Vorlesung eingeführt. Die Vorlesung "Verifikation eingebetteter Systeme" ist zwar hilfreich für das Verständnis, aber keine Voraussetzung. Lehrinhalte:
Für diese Klassen von Modellen werden Algorithmen besprochen, mit denen automatisch diverse Eigenschaften überprüft werden können wie zum Beispiel:
|
| Kommentar |
Spezialvorlesung für Bachelor/Master Informatik/ESE |