Development Methodology for Verifiable Adaptive Embedded Systems

The described project is part of the research cluster on “Dependable Adaptive Systems and Mathematical Modeling”.

Members

Prof. Dr. Peter Liggesmeyer, Fraunhofer-IESE
Prof. Dr. Arnd Poetzsch-Heffter, TU Kaiserslautern, AG Software Technology
Prof. Dr. Dieter Rombach, Fraunhofer-IESE
Prof. Dr. Klaus Schneider, TU Kaiserslautern, AG Reactive Systems

Abstract

The goal of the project is the development of new methods for modeling, analysis, and model-based synthesis of embedded systems that support dynamic adaptivity. We call a hardware-software system adaptive, if it can adapt its behavior and architecture to changing requirements of the environment. Since adaptations can affect different subsystems in parallel, techniques are needed that guarantee the correct functioning of the overall system at any point in time. A central topic of the project is the integration of modeling, design, analysis, verification, simulation, and testing methods for adaptive systems. In particular, we address the following areas of research:

Languages for adequate modeling of adaption and functionality of embedded systems
Quantitative safety and dependability analysis
Analysis and verification of safety properties of adaptive system models
Model-based synthesis from adaptive system models
Implementation verification of adaptive systems
Concepts for adaptive architectures

Within this project, the Software Technology Group focuses on language aspects for formal modeling of adaption and on a framework for integrating modeling techniques with existing verification methods.