Systemsoftware und Verteilte Systeme

AVACS - Subprojekt S3: Verifikation von Verlässlichkeitseigenschaften

Beginn des Projekts 2007, Ende des Projekts 2016

Beschreibung

Dieses Projekt beschäftigt sich mit der Entwicklung von Methoden zur Quantifizierung und Erweiterung von Eigenschaften selbststabilisierender Systeme. Um die Entwicklung selbststabilisierender Systeme auch Nicht-Experten zu ermöglichen, müssen solche Methoden soweit wie möglich automatisiert werden. Die zugrunde liegenden Modelle für die Analyse- und die Re-Engineering-Methoden sind zeitlich-diskrete Markowketten (Discrete Time Markov Chains, DTMC) sowie zeitlich-diskrete Markow Entscheidungsprozesse (Discrete Time Markov Decision Processes, DTMDP). Ein Problem der Analyse selbststabilisierender Systeme basiert auf der Tatsache, dass die Anzahl möglicher initialer Zustände gleich der Anzahl aller möglichen Zustände ist. Daher werden Abstraktionsschemata und semantische Modelle entwickelt, um diese Probleme, die während der Analyse auftreten, zu überwinden. Es ist unmöglich, eine Prozedur zu definieren, welche die gesamte Klasse der selbststabilisierenden Systeme abdeckt. Daher werden selbststabilisierende Systeme entsprechend ihres Verhaltens klassifiziert und für die einzelnen Subklassen Beweisverpflichtungen ausgearbeitet. Weiterhin werden Fehlertoleranzmetriken zur Quantifizierung des Verhaltens selbststabilisierender Systeme eingeführt. Oft wird der avisiserte Grad an Fehlertoleranz durch mangelnde Implementierungserfahrung für selbststabilisierende Systeme nicht erreicht. Daher ist es von Bedeutung, dieses Wissen bei der Implementierung von Szenarien auszunutzen. Im Rahmen dieses Projekts werden Gegenbeispiele, die durch Analysemethoden erstellt werden, benutzt, um ein System zu überarbeiten, so dass eine spezifizierte Servicequalität erreicht wird (Abbildung). Weiterhin wird angestrebt, Heuristiken zu ermitteln, so dass der Zustandsraum eines Szenarios in einem Gegenbeispiel auf ein Modifizierungsprotokoll abgebildet werden kann um die Fehlertoleranzmetriken zu verbessern.

Personen