Timed Controller Synthesis: An Industrial Case Study

The design of controllers for embedded systems is a difficult engineering task. Controllers have to enforce properties like safety properties (e.g. “nothing bad will happen”), or reachability properties (e.g. “something good wi ll happen”), and ideally they should do that in an efficient way, e.g. consume the least possible amount of energy. The foundations of automatic synthesis of discrete and timed controllers have been presented in the preceding chapter 1. In this chapt er, we illustrate the application of these approaches with an industrial case stu dy provided by the HYDAC ELECTRONIC GMBH company in the context of the European research project Quasimodo [7]. We present in the sequel how to use (in a system atic way) the tool UPPAAL -TIGA [1] (see chapter 1 for an introduction to the tool) for the s ynthesis, together with tools for the verification and the simulation o f a provable correct and near optimal controller for real industrial applications.