|Projektträger:||DFG (Deutsche Forschungsgemeinschaft)|
|Projektverantwortung vor Ort:||Dr. Hella Seebach|
|Beteiligte Wissenschaftler der Universität Augsburg:||
Dr. Hella Seebach
Dr. Florian Nafz
Dipl.-Inf. Jan-Philipp Steghöfer
|Publikationen:||Link zur Publikationsliste|
The project "Formal Modeling, Safety Analysis, and Verification of Organic Computing Applications (SAVE ORCA)" is part of the DFG - priority programme "Organic Computing".The subject of this project is 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 is to provide a formal framework for descriptive requirements, rigorous modeling and modular design of self-adapting and self-organizing systems. This will make 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 will be provided and prototypical tool support will be implemented. The method will be 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 focuses on the modeling and analysis of computer-controlled, technical systems. One approach is 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 is 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 modeled with EPF (Eclipse Process Framework Composer) and SPEM (Software Process Engineering Metamodel) respectively UMA (Unified Method Architecture) are availabled here. Additionally, we want to show how our guideline can be smoothly integrated in other software engineering process. Here you find an example of our guideline integrated into the Open Unified Process (Open UP).
ExampleAn example is a fully automated, organic production cell consisting of three robots. Every robot is equipped with 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 tasks are performed in the correct order (self-organizing). Each robot has tools for performing any of these tasks. However, switching the tools takes considerably more time than processing the workpiece. So each robot specializes on one task 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 task,
- communicates this to the other robots, so that they also switch tasks, 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.
Download sample movie in the download area below.