Overview

The project "Formal Modeling, Safety Analysis, and Verification of Organic Computing Applications (SAVE ORCA)" was part of the DFG - priority programme " Organic Computing".

The subject of this project was a method for the systematic, top-down design and construction of highly reliable and adaptive organic computing applications. Reliability here means preservation of functional correctness, safety and security under unexpected disturbances and component failures. Adaptability in the context of this project is related to adaptive system behavior under changing requirements and modified tasks. The aim was to provide a formal framework for descriptive requirements, rigorous modeling and modular design of self-adapting and self-organizing systems. This makes design and construction of future organic systems easier and safer. As an integral part of the framework, formal analysis will improve reliability, stability, and adaptability of such systems.

The approach combines formal specification and verification with failure analysis techniques and intelligent re-configuration. For specification standard modeling languages and tools like Cadence SMV, I-Logix Statemate and Esterel Technologies SCADE Suite are used. Verification is done with automatic model checking and interactive verification. Example applications are 'automation engineering' and 'mobile systems'. A formal framework for the analysis of organic computing applications is provided and prototypical tool support implemented. The method was evaluated with substantial case studies.

Relevant research can be grouped into three categories:

• Self-x properties: This category deals with the definition and integration of self-x properties, e.g. self-configuring, self-healing, self-optimizing, self-protecting, self-organization, self-regulation, self-repair, self-maintenance and self-diagonsis.
• System design and modeling: The benefit and necessity of system engineering approaches have become apparent -- not only for organic computing systems -- during the last years. For organic systems, formal system design and analysis is even more important, as emergence and self-x properties make these systems more complex, challenging to analyze, and system failure often results in great loss. Today no method, language and tool exists which can be used for design, analysis and simulation of embedded systems that have self-x capabilities.
• Formal safety analysis: The research in this area focused on the modeling and analysis of computer-controlled, technical systems. One approach was to use well-established safety analysis methods from engineering and enhance them with formal semantics. This allows to rigorously prove safety properties.

SAVE ORCA Guideline

One aim of the project was the systematic, top-down design and construction of self-organizing systems. Therefore, we developed a guideline that helps software engineers to design and construct self-organizing resource-flow systems.
The complete SAVE ORCA guideline is modeled with EPF (Eclipse Process Framework Composer) and SPEM (Software Process Engineering Metamodel) respectively UMA (Unified Method Architecture). Additionally, we showed how our guideline can be smoothly integrated in other software engineering process like the OpenUP.

Example

An example is a fully automated, self-organizing production cell consisting of multiple robots. Every robot is equipped with e.g. three tools for drilling a hole, tightening a screw and cutting the end of the screw. The workpieces are carried by holonic transport units (carts) between the robots, so that the three tools are performed in the correct order (self-organizing). Switching the tools takes considerably more time than processing the workpiece. So each robot specializes on one tool and carts transport the workpieces from robot to robot (self-optimizing). If any of the robots recognizes a failure in its current tool then the system uses its self-healing capabilities, i.e.

• the handicapped robot switches to another tool,
• communicates this to the other robots, so that they also switch there assigned tools, and that
• the carts modify their itinerary because the pieces must be carried around in a different order.

We implemented the production cell within Jadex, a multi agent platform.

Funded by

Key Facts

Start date:

01.07.2005

End date:

30.06.2011

Duration:

6 years