Effiziente Verifikation von Performability-Eigenschaften verteilter Systeme

• Antragsteller: Professor Dr.-Ing. Markus Siegle
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2003 bis 2010
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5405376

Für die Performability-Analyse (d.h. die kombinierte Leistungs- und Zuverlässigkeitsanalyse) verteilter Systeme kann man sehr gut stochastische Prozessalgebren (SPA) einsetzen. Dabei wird das Verhalten der beteiligten Komponenten und deren Kooperation durch eine formale Spezifikation modelliert, die anschließend gemäß einer formalen Semantik in eine beschriftete, zeitkontinuierliche Markovkette überführt wird. Schließlich wird die Markovkette mit Hilfe numerischer Methoden analysiert, so dass die gewünschten Performability-Maße ermittelt werden können. In den letzten Jahren wurden temporale Logiken für stochastische Systeme und zugehörige Verifikationsverfahren (samt Pilotimplementiertungen) entwickelt, mit deren Hilfe sowohl funktionale als auch Performability-orientierte Eigenschaftsklassen von SPAs formal spezifiziert und automatisch verifiziert werden können. Ein solches Vorgehen hat den Vorteil, dass die Spezifikation des Systems und der zu verifizierenden Eigenschaften auf demselben hohen Abstraktionsniveau stattfinden kann. An diesen Entwicklungen war unsere Arbeitsgruppe, etwa durch die Entwicklung der Logik ACSL und des SoftwareWerkzeugs ETMCC, federführend beteiligt. Das mit dem hier beantragten Vorhaben verfolgte Ziel ist es nun, die Klasse der beschreib- und analysierbaren Performability-Eigenschaften stark zu erweitern. Dazu soll eine sehr allgemeine aktionsbasierte temporale Logik zur Spezifikation von Performability-Maßen definiert werden. Weiterhin sollen Verfahren zur vollautomatischen quantitativen Verifikation der temporallogischen Formeln entwickelt werden. Beim Entwurf dieser Model-Checking-Algorithmen steht die Effizienz im Vordergrund, da die Modellierung moderner verteilter Systeme leicht zu unbeherrschbar großen Zustandsräumen führt. Dazu wollen wir eine mögliche Reduktion des Zustandsraums sowie dessen kompakte Darstellung im stochastischen Kontext untersuchen.

• DFG-Verfahren: Sachbeihilfen