Completed on 28 March 2006 by Baltin Karro.

• Prof. Dr.-Ing. Oliver Theel
• Dipl.-Inform. Jens Oehlerking
• Dipl.-Inform. Henning Burchardt
  

• Hybrid systems
• Verification

The property of system stability plays a central role in the control of technical systems. Whenever a system is brought into an undesirable state by disturbance effects, it should be automatically ensured that the system is brought back into a desirable state(i.e. stabilises). Examples of such systems include heating systems, speed control systems on vehicles or the control of chemical processes. Such control systems are usually modelled using differential equations, and mathematical methods exist to prove stability.

Hybrid systems are a special class of control systems that are characterised by the fact that they have different modes in which the system behaves in fundamentally different ways. Due to their flexibility, these technical systems are of great interest in development and research. The AVACS Collaborative Research Centre, on which this work is based, applies verification techniques to railway control systems. In particular, a tool for automatic stability verification for such systems is to be developed. The existing algorithms for such hybrid systems are only capable of verifying certain types of hybrid systems. Therefore, systems must be classified into different categories.

Based on given specifications of hybrid systems, a tool is to be developed that classifies these systems according to predefined criteria (time-invariant, constant/linear in each mode, deterministic, linear switching logic). Logical formulae and differential equations must be analysed for this purpose. The tool should be easily extendable by further classes to be identified.

• Knowledge of C/C++
• Basic knowledge of maths and logic

The work contains practical components. There is also the opportunity to visit partner universities or institutes within AVACS (Universities of Freiburg and Saarbrücken, Max Planck Institute Saarbrücken).