Quantitative Verification - Sommersemester 2020
Übersicht
| Beschreibung |
Die klassische funktionale Verifikation ("Das System wird immer einen sicheren Zustand erreichen") liefert oft unbefriedigende Ergebnisse: Werden Nachrichten über eine unzuverlässige Verbindung übertragen, können einzelne Pakete verloren gehen, egal wie oft die Übertragung wiederholt wird; bei einem Flug besteht immer eine von Null verschiedene Wahrscheinlichkeit, dass eine kritische Situation eintritt. Somit würde die "klassische" Verifikation in beiden Fällen das System als unsicher einstufen. Allerdings macht es sehr wohl einen Unterschied, ob im Flugzeug die kritische Situation mit Wahrscheinlichkeit 10-2 oder 10-10 eintritt. Im ersten Fall würde man das Flugzeug besser nicht nutzen, im zweiten wäre das Risiko sehr überschaubar. Das Ziel der Vorlesung "Quantitative Verification" ist es, Modelle und Algorithmen zu entwickeln, die es erlauben, Sicherheitseigenschaften quantitativ zu untersuchen und Kostenmaße zu berechnen ("Wie lange dauert es im Mittel, bis die Nachricht angekommen ist?). |
| Kommentar |
Spezialvorlesung in den Bachelor- und Masterstudiengängen Informatik und ESE. |