Entwurf und (quantitative) Analyse Komponenten-basierter Systeme
Zusammenfassung der Projektergebnisse
Das Projekt widmete sich dem Entwurf und der theoretischen Analyse von Systemen, die aus Komponenten aufgebaut sind. Als Basis zur Beschreibung Komponenten-basierten Systeme wurden Interaktionssysteme herangezogen, ein Modell, das von Goessler und Sifakis entwickelt wurde. Wichtig ist dabei, dass Komponenten abgeschlossene, unabhängige Einheiten sind, die sich nicht auf andere Komponenten beziehen können. Jede Komponente bietet für die Kooperation mit der Umgebung sogenannte Ports an. Komponenten werden mittels eines Glue Codes, der die Ports benutzt, zu Komponentensystemen zusammengesetzt. Im Projekt stand die komplexitätstheoretische Analyse und der Entwurf von Algorithmen zum Nachweis wichtiger Eigenschaften derartiger Systeme im Vordergrund. Die Ergebnisse können wie folgt zusammengefasst werden: Es wurde gezeigt, dass die Überprüfung von wichtigen Eigenschaften, wie z.B. Verklemmungsfreiheit, Komponenten-basierter Systeme PSPACE-vollständig ist. Eine Möglichkeit mit dieser Situation umzugehen besteht darin, Bedingungen aufzustellen, die in polynomieller Zeit überprüfbar sind und eine gewünschte Eigenschaft implizieren. Damit ist für ein System, das die hinreichende Bedingung erfüllt, die Aufgabe gelöst. Ist die Bedingung nicht erfüllt, kann man die, beim Versuch des Nachweises derselben, gewonnenene Information z.B. in einen nachfolgenden Model Checking Schritt einfließen lassen, um ein definitives Endergebnis zu erhalten. Wir entwickelten Bedingungen für Fortschritt, Verklemmungsfreiheit und Robustheit von Eigenschaften gegenüber dem Ausfall von Diensten. Ein wichtiger Aspekt bei unseren Untersuchungen ist die Interaktionsstruktur des Komponentensystems, die beschreibt, welche Komponenten mit welchen anderen Komponenten mittels des Glue Codes interagieren. Dabei kommt Systemen, die eine baumartige Interaktionsstruktur aufweisen, eine besondere Bedeutung zu. Zunächst konnten wir zeigen, dass selbst für diese eingeschränkte Klasse von Systemen die Überprüfung von Eigenschaften PSPACE-vollständig ist. Auf der anderen Seite kann man unter gewissen Bedingungen die Analyse baumartiger Systeme kompositional durchführen, indem man nur Paare benachbarter Komponenten, d.h. interagierender Komponenten, betrachtet. Ein wichtiger Aspekt unserer Untersuchungen ist, dass die aufgestellten Bedingungen auch als Richtlinien für Systementwurf interpretiert werden können. Gelingt es beim Systementwurf z.B. eine Bedingung für Verklemmungsfreiheit einzuhalten, so ist das System “ deadlock-free by construction”. Die aus den Bedingungen konstruierten Algorithmen wurden implementiert. Die Arbeiten werden u.a. in einem anderen DFG Projekt weitergeführt.
