Quantitative Modellprüfung | Das Universitätsnetzwerk

Beschreibung

Die Integration von IKT (Informations- und Kommunikationstechnologie) in verschiedene Anwendungen nimmt rasch zu, beispielsweise in eingebetteten und cyberphysischen Systemen, Kommunikationsprotokollen und Transportsystemen. Daher hängt ihre Zuverlässigkeit und Zuverlässigkeit zunehmend von Software ab. Defekte können fatal und äußerst kostspielig sein (im Hinblick auf die Massenproduktion von Produkten und sicherheitskritischen Systemen).

Zunächst muss ein Modell des realen Systems erstellt werden. Im einfachsten Fall spiegelt das Modell alle möglichen Zustände wider, die das System erreichen kann, und alle möglichen Übergänge zwischen Zuständen in einem (bezeichneten) Zustandsübergangssystem. Beim Hinzufügen von Wahrscheinlichkeiten und diskreter Zeit zum Modell haben wir es mit sogenannten zeitdiskreten Markov-Ketten zu tun, die wiederum mit kontinuierlichem Timing zu zeitkontinuierlichen Markov-Ketten erweitert werden können. Beide Formalismen werden häufig zur Modellierung und Leistungs- und Zuverlässigkeitsbewertung von Computer- und Kommunikationssystemen in einer Vielzahl von Bereichen verwendet. Diese Formalismen sind gut verstanden, mathematisch attraktiv und gleichzeitig flexibel genug, um komplexe Systeme zu modellieren.

Bei der Modellprüfung steht die qualitative Bewertung des Modells im Mittelpunkt. Als formale Verifizierungsmethode dienen Model-Checking-Analysen
die Funktionalität des Systemmodells. Eine zu analysierende Eigenschaft muss in einer Logik mit konsistenter Syntax und Semantik angegeben werden. Für jeden Zustand des Modells wird dann geprüft, ob die Eigenschaft gültig ist oder nicht.
Der Schwerpunkt dieses Kurses liegt auf der quantitativen Modellprüfung für Markov-Ketten, für die wir effiziente Rechenalgorithmen diskutieren. Die Lernziele dieses Kurses sind wie folgt:

– Drücken Sie Zuverlässigkeitseigenschaften für verschiedene Arten von Übergangssystemen aus.
– Berechnen Sie die zeitliche Entwicklung für Markov-Ketten.
– Prüfen Sie, ob einzelne Staaten eine bestimmte Formel erfüllen und berechnen Sie die Erfüllungsmenge für Eigenschaften.