Quantitative modeling and analysis of service-oriented real-time systems using interval probabilistic timed automata

Meer over het boek

Eine der größten Herausforderungen bei der Entwicklung von service-orientierten Systemen ist die Vorhersage und Sicherstellung nicht-funktionaler Eigenschaften wie Ausfallsicherheit und Verfügbarkeit interorganisationeller Dienste. Diese Systeme sind oft durch zahlreiche Unsicherheiten geprägt, die sowohl in der Modellierung als auch in der Analyse eine Rolle spielen. Die relevanten Unsicherheiten lassen sich in epistemische Unsicherheiten, die durch unvollständiges Wissen entstehen, und Zufallsfaktoren, die in Protokollen oder physikalischen Prozessen auftreten, unterteilen. In diesem Bericht wird ein probabilistisches, zeitbehaftetes Modell untersucht, das quantitative Aussagen über nicht-funktionale Eigenschaften einer bestimmten Klasse von service-orientierten Echtzeitsystemen ermöglicht. Ein Anforderungskatalog für probabilistische Echtzeitsysteme mit Unsicherheiten wird erstellt, um die Auswirkungen dieser Unsicherheiten auf die Wahl der Modellierungs- und Analysemethoden zu verdeutlichen. Als formales Modell kommen Interval Probabilistic Timed Automata (IPTA) zum Einsatz. Das Modell bietet die notwendige Ausdrucksstärke für eine realistische Spezifikation und geeignete Methoden zur Bestimmung quantitativer Sicherheits- und Zuverlässigkeitseigenschaften. Für die quantitative Analyse wird probabilistisches Model Checking verwendet, unterstützt durch eine Erweiterung des Prism-Werkzeugs zur Modellierung und Analyse von IPT