Quantitative Verification

Worum geht's

Du lernst, wie man Systeme mit quantitativen Aspekten (z. B. Zeit, Wahrscheinlichkeiten) formal modelliert und analysiert. Am Ende kannst du geeignete Modellklassen und Spezifikationssprachen anwenden, Analysealgorithmen erklären und auf kleine Beispiele praktisch nutzen sowie Modellprüfungswerkzeuge einsetzen.

Was du danach kannst

• Rolle quantitativer Modellierung und Analyse für Hardware-/Softwarequalität erklären
• formale Modelle probabilistischer und zeitlicher Systeme erstellen
• formale Spezifikationen für Sicherheit, Zuverlässigkeit und Leistung formulieren
• Algorithmen zur Überprüfung von Systemen erklären und auf kleine Beispiele anwenden
• Techniken zur Verbesserung der praktischen Leistungsfähigkeit von Analysealgorithmen verstehen und erklären

Aus was das Modul besteht

• VorlesungVermittlung der Grundlagen; während der Vorlesungen werden kleine Aufgaben online gelöst
• Übung/TutorialBesprechung der wöchentlichen Aufgaben und Vertiefung durch Beispiele

Lehrmethode

• VorlesungEinführung in Theorie und Algorithmen, Online-Übungsaufgaben während der Veranstaltung
• Tutorial/ÜbungDiskussion und Lösung der wöchentlichen Aufgaben zur Festigung
• Tool-PräsentationPraktische Erfahrung mit Model-Checking-Werkzeugen (z. B. PRISM, MRMC, UPPAAL)