Execution Monitor Synthesis for Hybrid Systems

Formal verification methods for hybrid controllers have received a lot of attention during the last decade and so has the problem of synthesizing specifications of hybrid controllers. Such specifications do then fulfill given requirements, such as timing constraints or safety properties. However, the problem of automatically implementing the actual control programs has received much less attention, and one of the reasons for this is that industrial controllers necessarily have to be able to effectively handle every conceivable situation that might occur in reality, which make the construction of the specification very difficult. In this preliminary report, we take one step towards automatic generation of control systems by proposing that not only the control program should be synthesized from a specification, but also an Execution Monitor that is able to detect and classify discrepancies between the model of the closed-loop system and the actual effects of control actions. We show how..