Effiziente Verifikation von Performability-Eigenschaften verteilter Systeme

性能分析（d.h.这种混合动力系统可以使人进行随机过程（SPA）。Dabei wird das Verhalten der beteiligten Komponenten und deren Cooperation durch eine Spezifikation modelliert，die anschließend gemänner formalen Semantik in eine beschriftete，zeitkontinuierliche Markovsküberführt wird. Schließlich将使用Hilfe数值方法分析马尔可夫模型，从而使性能最大化韦尔登。在过去的几年里，我们将暂时对随机系统进行Logiken für stochastische Systeme und zugehörige Verifikationsverfahren（samt Pilotimplementiertungen）的设计，其中，我们的医疗服务功能也将使SPA的性能导向的特征验证正式化，并进行韦尔登。一个问题是，系统的特性和特征的验证可以在抽象的统计中找到。这一发展是我们工作组的一项工作，它是通过Logik ACSL和Software Werkzeugs ETMCC的发展而实现的。由于采用了这种方法，Ziel的性能特征分析和性能评价指标非常明显。这是一个非常普遍的基于时间的逻辑，用于确定韦尔登的性能指标。还需要对时间表进行量化验证，以确定韦尔登。由于模型检验方法在前向建模中的有效性，使得现代虚拟系统的建模变得非常简单。大足将在随机语境中进行一次大规模的空间缩减。

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.