Verhaltenstheorie und Logik für Verteilte Adaptive Systeme

Ein verteiltes, adaptives System ist ein System, das aus kommunizierenden, autonomen Komponenten zusammen gesetzt ist. Das Verhalten der Komponenten kann dabei unbeständig sein, d.h. Komponenten können ausfallen, aufgrund von Netzwerkfehlern unerreichbar sein oder auch ihr Verhalten ändern. Also muss das System anpassungsfähig sein, um Fehlverhalten zu erkennen, sich selbst an neue Situation anzupassen und zur Normalverarbeitung zurückzukehren sobald ein Fehler behoben ist. Folglich sind die Überwachung der Systemumgebung und die Verhaltensanpassung an kritische Situationen definierende Eigenschaften verteilter, adaptiver Systeme. Zum Beispiel kann eine Produktionszelle mehrere autonome Systeme (z.B. Steuerungen für Schweißroboter) umfassen, die eine gemeinsame Aufgabe erledigen (z.B. eine Schweißaufgabe in der Automobilproduktion). Diese Systeme können miteinander kommunizieren, um herauszufinden, ob alle Komponenten ordnungsgemäß arbeiten, und einen Konsenz herbeizuführen, wann die Aufgabe abgeschlossen ist. Verhält sich eine Komponente fehlerhaft, dann sollten die übrigen Komponenten den Fehler erkennen können, die fehlerhafte Komponente isolieren und signalisieren, dass diese zu ersetzen ist, und die Aufgabe falls möglich unter sich neu verteilen. Sobald dem System mitgeteilt wird, dass die fehlerhafte Komponente ersetzt oder repariert wurde, könnte das System zur ursprünglichen Arbeitsverteilung zurückkehren. Verschiedene Produktionszellen könnten in einer Produktionslinie zusammengefasst sein, die durch ein weiteres verteiltes, adaptives System mit mehr Anpassungsfreiraum, z.B. durch Veränderung der Arbeitsreihenfolge, Nutzung von Unterstützungskomponenten, etc. gesteuert wird. Dies kann noch weiter auf Fabrikebene mit mehreren Produktionslinien bis hin zur gesamten Produktion eines produzierenden Unternehmens mit mehreren Fabriken ausgebaut werden. Das Ziel des Projekts ist es, solide wissenschaftliche Grundlagen solcher verteilter, adaptiver Systeme unter Erfassung aller Aspekte durch einen schrittweisen Ansatz zu schaffen. Das Projekt soll klären, was verteilte, adaptive Systeme genau sind, wie sie spezifiziert werden können, wie Eigenschaften wie Verlässlichkeit, Ausfallsicherheit und Robustheit garantiert werden können und wie sie klassifiziert werden können. Hierfür wird der Begriff der "Verhaltenstheorie" aus Gurevich`s richtungsweisenden Arbeit zur ASM These und Nachfolgearbeiten zur sprachunabhängigen Charakterisierung von Klassen von Algorithmen adaptiert.

Ein verteiltes System besteht aus mehreren autonomen Softwarekomponenten, die über ein Netzwerk verteilt sind. Die Komponenten kooperieren über gemeinsame Speicherplätze und Mitteilungen. Autonomie bedeutet, dass die einzelnen Komponenten völlig unabhängig von- einander agieren und nicht mehr wissen als das die Inhalte der gemeinsamen Speicherplätze auch von anderen genutzt werden. Ein solches verteiltes System ist adaptiv, wenn die einzelnen Komponenten ihr Verhalten, d.h. das ihnen zugeordnete Programm, zur Laufzeit selbst verändern können. Wenn z.B. eine Komponente zerbricht, oder der entsprechende Knoten im Netzwerk nicht mehr zuganglich ist oder wenn eine Komponente mit abweichendem Verhalten zum Gesamtsystem beitritt, können anderen Komponenten dieses erkennen und sich an die neue Situation anpassen. Deshalb sind die Beobachtung der Systemumgebung und dessen Anpassung an kritische Situationen charakterisierend für verteilte, adaptive Systeme.Eine Produktionszelle mag z.B. mehrere autonome Systeme enthalten, die die Ausführung einer gemeinsamen Aufgabe steuern. Die einzelnen Komponenten würden dann miteinander kommunizieren, um festzustellen, ob alle Komponenten ordungsgemäß arbeiten, und einen Konsenz herbeiführen, wann die Aufgabe als erledigt zu betrachten ist. Falls eine Komponente fehlerhaft ist, müssen die anderen dies erkennen, die fehlerhafte Komponente isolieren, signalisieren, dass sie zu ersetzen ist und die Teilaufgabe der fehlerhaften Komponente anderweitig zuweisen, sofern dieses möglich ist. Sobald die fehlerhafte Komponente repariert oder ausgetauscht wurde und dieses dem System mitgeteilt wurde, kann zur ursprünglichen Arbeitsverteilung vor Auftreten des Fehlers zurückgekehrt werden.Das erste Hauptergebnis des Projekts ist eine Verhaltenstheorie für solche verteilten, adaptiven Systeme. Die Theorie umfasst erstens eine sprachunabhängige Charakterisierung durch wenige intuitive Postulate, die von bekannten Formalismen erfüllt werden, zweitens ein abstraktes Maschinenmodell, das die Postulate erfüllt, und drittens den mathematischen Beweis, dass alle durch die Postulate zugelassenen Systeme durch das abstrakte Maschinenmodell treu repräsentiert werden können. Diese Verhaltenstheorie ermöglicht es, jedes verteilte, adaptive System durch eine konkrete Sprache für das abstrakte Maschinenmodell zu spezifizieren.Das zweite Hauptergebnis ist eine Logik für verteilte, adaptive Systeme auf der Basis des abstrakten Maschinenmodells, die es erlaubt, formal wünschenswerte Eigenschaften, die eine Systemspezifikation erfüllen muss, zu formulieren und mathematisch zu verifizieren. Insbesondere wird durch diese Logik statische Verifikation von Systemeigenschaften nach beliebig vielen Anpassungsschritten möglich.