Cluster of Excellence: Dependable Adaptive Systems and Mathematical Modeling (DASMOD)

Software systems play crucial roles in modern societies, in particular in the form of embedded systems and information systems. In the future, they need to adapt automatically to the available system resources, to the environment, and to the user. Mathematical models allow to describe the real world as well as the interaction with the software systems and, in particular, to express probabilistic process behavior. Simulations and visualizations can be used to validate those models. Being complex software systems on their own, simulation systems form ideal prototype testbeds for embedded and other environment-dependent adaptive software systems. This role of simulation software will become more and more strengthened in the future.

The general aim of this research cluster is to further integrate software system engineering, mathematical modeling, and simulation and to provide the foundation for understanding and constructing the future generation of adaptive systems. This basic foundation is required to enable the society to exploit the power of such systems, and also to estimate the risks of being dependent on those systems in many aspects.

Cluster Project: Verification and Simulation of Embedded Hybrid Systems (VerSiS)

Formal verification is crucial in the design process of reliable embedded systems. The particular challenge is due to the heterogeneity of the involved technical systems. Despite of custom digital hard- and software components, also actuator and sensor componets play an important role as interfaces to the environment. The development of new design and verification methods with integrated work flow is the main subject of this project.

The close cooperation of the involved working groups, whose main competences reflect various aspects of hybrid embedded systems, is the essential condition for putting into practice this reasearch project. The approaches developed by the Reactive Systems Group will be extented for describing analog systems, which obey differential equations.

Starting with these hybrid programs a description for simulation, verification and generation of hard- and software will be obtained. For verification of digital subsystems computational methods by the Algebra, Geometry and Computer Algebra Group will be used, which reduce Boolean problems to equivalent problems in polynomial rings.

Sensor and actuator components will be verfied using methods developed by the department System Analysis, Prognosis and Control. In particular efficient symbolic methods should be applied for verification of tolerance-affected components, together with new interval arithmetical approachs on the one hand, and modern modelling techniques for multi-physical systems on the other.

Finally, the developed methods should be evaluated with respect to case scenarios from the area of robotics, which will be provided by examples of the behaviour based control of the Robotics Laboratory.