Verification and Simulation of self-optimizing mechatronic Systems

Self-optimizing mechatronic systems adapt their software to their changing environment by themselves. This is called reconfiguration. If several mechatronic systems interact with each other, then the communications links and the number of communication partners of a systems may change during run-time as well. For using such systems in safety-critical environments, a correct behavior of the system must be guaranteed to enable safe operations.

One method for guaranteeing the correctness of a system with respect to its specification is model-driven software engineering. That enables the use of formal methods to proove the correctness of the system. The integration of discrete software  with mechanical and control engineering models may be checked using simulation-based approaches.

In this PhD project, different methods and algorithms are developed that enable formal verification and simulation of self-optimizing mechatronic systems. It is necessary that the formal verification considers the reconfiguration of the system in order to retrieve valid results. In course of the verification, the complete system behavior is transformed into timed graph transformation systems that are then verified by a model checking approach.

The simulation of a reconfigurable system model is not supported natively by simulation tools like Matlab/Simulink or Dymola/Modelica. Enabling simulation for such systems requires a suitable encoding of the system model such that it may be used inside the simulation environment.

The methods and algorithms that are created in this PhD project are implemented based on the Fujaba Realtime Tool Suite.

Contact: Christian Heinzemann