?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

?