  In this paper, we propose a novel framework for the synthesis of robust and
optimal energy-aware controllers. The framework is based on energy timed
automata, allowing for easy expression of timing constraints and variable
energy rates. We prove decidability of the energy-constrained infinite-run
problem in settings with both certainty and uncertainty of the energy rates. We
also consider the optimization problem of identifying the minimal upper bound
that will permit the existence of energy-constrained infinite runs. Our
algorithms are based on quantifier elimination for linear real arithmetic.
Using Mathematica and Mjollnir, we illustrate our framework through a real
industrial example of a hydraulic oil pump. Compared with previous approaches
our method is completely automated and provides improved results.
