Repairing Control Safety Violations via Scheduler Patch Synthesis

Cyber-physical systems are typically implemented in software as a set of real-time control tasks. Timing uncertainty at the low-level scheduling layer can lead to deadline misses of control tasks, that affects control performance and may violate safety properties associated with the high-level control applications. We present a technique to detect and repair control safety violations by synthesizing a scheduler patch - a pre-computed list of jobs to be not scheduled at runtime - that eliminates these violations without the need of modifications at the control or task layer. The technique utilizes a guess-check-repair loop on top of an exact SMT encoding of control and scheduling behaviours, enabling efficient packing of multiple control applications on the execution platform while guaranteeing control safety.