Analysis and synthesis of hybrid systems in engineering applications

This thesis deals with analysis and synthesis methods and their application in the area of engineering. In the first part, we show the application of formal methods in chemical plant control to verify safety critical properties. In general, not only the control program but also the controlled system are relevant to prove a set of requirements. Thus, we show how a hybrid automaton can be generated automatically, that models the controller, its cyclic execution, and the dynamic plant behavior.We propose verification techniques based on counterexample-guided abstraction refinement (CEGAR) to keep the model sizes moderate. However, existing analysis tools do not compute counterexamples for models beyond timed automata. Thus, we present different methods to over-approximate the set of counterexamples for hybrid automata and we employ simulation techniques to validate counterexamples.Afterwards, we develop two CEGAR approaches for our application scenario. The first one starts with an analysis on a purely discrete model. For each discrete counterexample, a reachability analysis that is guided along the discrete counterexample is computed on the hybrid system model. The second approach uses reachability analysis for hybrid systems and abstracts away parts of the dynamic plant behavior.Finally, we show that some special characteristics of our models can be exploited during the analysis to reduce the computation time and to increase the accuracy of the computed reachable state set.In the second part of this thesis, we switch to the synthesis of control strategies for parallel hybrid vehicles where an internal combustion engine and an electrical motor are coupled on the same axis. A control strategy distributes the requested torque over the available engines.We implement a control strategy that optimizes the control using a GA. The basis of this control strategy is our GA library GeneiAL. We analyze the control strategy to determine real-time capable configurations with good optimization results. For promising configurations, we compare the GA-based control strategy with common control strategies. Moreover, we report on the integration of this set of control strategies into a learning-based control strategy. A learning-based control strategy optimizes the fuel consumption using a set of control strategies as experts. We can show that the fuel consumption of the learning-based control strategy is comparable to the fuel consumption of the best expert. On all benchmarks, GA-based control strategies turn out to be the best experts