Überblick

Das Projekt "Formale Modellierung, Sicherheitsanalyse und Verifikation von Organic Computing Anwendungen (SAVE ORCA)" war Teil des DFG-Schwerpunktprogramms " Organic Computing".

Gegenstand dieses Projekts war die Entwicklung einer Methodik für das systematische, top-down Design und die Konstruktion von hochzuverlässigen und adaptiven Computeranwendungen. Zuverlässigkeit bedeutet hier den Erhalt der funktionalen Korrektheit, der Sicherheit und des Schutzes bei unerwarteten Störungen und Komponentenausfällen. Die Anpassungsfähigkeit im Rahmen dieses Projekts bezieht sich auf das adaptive Systemverhalten bei sich ändernden Anforderungen und veränderten Aufgaben. Ziel war es, einen formalen Rahmen für deskriptive Anforderungen, rigorose Modellierung und modularen Aufbau von selbstanpassenden und selbstorganisierenden Systemen zu schaffen. Dies macht die Planung und den Bau zukünftiger selbstorganisierender Systeme einfacher und sicherer. Als integraler Bestandteil des Rahmens wird die formale Analyse die Zuverlässigkeit, Stabilität und Anpassungsfähigkeit solcher Systeme verbessern.

Der Ansatz kombiniert formale Spezifikation und Verifikation mit Fehleranalyseverfahren und intelligenter Rekonfiguration. Für die Spezifikation werden Standard-Modellierungssprachen und Tools wie Cadence SMV, I-Logix Statemate und Esterel Technologies SCADE Suite verwendet. Die Verifikation erfolgt durch automatische Modellprüfung und interaktive Verifikation. Anwendungsbeispiele sind "Automatisierungstechnik" und "Mobile Systeme". Ein formaler Rahmen für die Analyse von Organic Computing Anwendungen wird bereitgestellt und prototypische Werkzeugunterstützung implementiert. Die Methodik wurde mit umfangreichen Fallstudien bewertet.

Relevante Forschung kann in drei Kategorien eingeteilt werden:

• Self-x Eigenschaften: Diese Kategorie beschäftigt sich mit der Definition und Integration von Self-X-Eigenschaften, z.B. selbstkonfigurierend, selbstheilend, selbstoptimierend, selbstschützend, selbstorganisierend, selbstregulierend, selbstreparierend, selbstunterhaltend und selbstdiagnostisch.

• Systemdesign und Modellierung: Der Nutzen und die Notwendigkeit von System Engineering Ansätzen haben sich in den letzten Jahren - nicht nur für Organic Computing Systeme - gezeigt. Für selbstorganisierende Systeme ist das formale Systemdesign und die Analyse noch wichtiger, da Emergenz und Self-X-Eigenschaften diese Systeme komplexer machen, die Analyse schwierig ist und Systemausfälle oft zu großen Verlusten führen. Bisher gab es keine Methodik, Sprache oder Werkzeug, die für das Design, die Analyse und die Simulation von eingebetteten Systemen mit Self-X-Fähigkeiten verwendet werden konnte.

• Formale Sicherheitsanalyse: Die Forschung in diesem Bereich konzentrierte sich auf die Modellierung und Analyse computergesteuerter, technischer Systeme. Ein Ansatz bestand darin, etablierte Sicherheitsanalysemethoden aus dem Ingenieurwesen zu verwenden und durch formale Semantik zu ergänzen. Dies ermöglicht den strengen Nachweis von Sicherheitseigenschaften.

SAVE ORCA-Richtlinie

Ein Ziel des Projekts war die systematische, top-down Planung und Konstruktion von selbstorganisierenden Systemen. Deshalb haben wir einen Leitfaden entwickelt, der Softwareentwicklern hilft, selbstorganisierende Ressourcenflusssysteme zu entwerfen und zu konstruieren.
Die vollständige SAVE ORCA-Richtlinie ist mit EPF (Eclipse Process Framework Composer) und SPEM (Software Process Engineering Metamodel) bzw. UMA (Unified Method Architecture) abgebildet. Darüber hinaus haben wir gezeigt, wie sich unser Leitfaden nahtlos in andere Softwareentwicklungsprozesse wie den OpenUP integrieren lässt.

Beispiel

Ein Beispiel ist eine vollautomatische, selbstorganisierende Fertigungszelle, die aus mehreren Robotern besteht. Jeder Roboter ist mit z.B. drei Werkzeugen ausgestattet, um ein Loch zu bohren, eine Schraube einzusetzen und die Schraube anzuziehen. Die Werkstücke werden von holonischen Transporteinheiten zwischen den Robotern transportiert, so dass die drei Werkzeuge in der richtigen Reihenfolge ausgeführt werden (selbstorganisierend). Das Wechseln der Werkzeuge dauert wesentlich länger als die Bearbeitung des Werkstücks. So ist jeder Roboter auf ein Werkzeug spezialisiert und die mobilen Einheiten transportieren die Werkstücke von Roboter zu Roboter (selbstoptimierend). Erkennt einer der Roboter einen Fehler in seinem aktuellen Werkzeug, nutzt das System seine Selbstheilungskräfte, d.h.

• der „defekte“ Roboter wechselt zu einem anderen Werkzeug,
• kommuniziert dies den anderen Robotern, so dass sie auch ihre zugeteilten Werkzeuge wechseln, und 
• unterrichtet die Transporteinheiten, dass sie ihre Route ändern, da die Stücke in einer anderen Reihenfolge transportiert werden müssen.

Wir haben die Produktionszelle in Jadex, einer Multiagentenplattform, implementiert.

Förderung

Eckdaten

Start:

01.07.2005

Ende:

30.06.2011

Laufzeit:

6 Jahre