Statistical Approach to Efficient and Deterministic Schedule Synthesis for Cyber-Physical Systems

Correctness of controller implementations rely on real-time guarantees that all control tasks finish execution by their prescribed deadlines. However, with increased complexity and heterogeneity in hardware, the worst-case execution time estimates are becoming very conservative. Thus, for efficient usage of hardware resources, some control tasks might have to miss their deadlines. Recent work has shown that a system can still abide by its safety requirements even after missing some of its deadlines. This paper investigates an approach to synthesize a scheduler for control tasks that miss some deadlines without compromising its safety requirements. But given that the number of possible schedules increase combinatorially with the number of tasks involved, our scheduler synthesis uses an efficient automata representation to search for the appropriate schedule. We incorporate statistical verification techniques to construct this automaton and accelerate the search process. Statistical verification is advantageous compared to deterministic verification in the synthesis process in two ways: first, it enables us to synthesize schedules that would not be possible otherwise, and second, it drastically reduces the time taken to synthesize such a schedule. We demonstrate both these advantages through a case study with five controllers having different safety specifications, but sharing the same computational resource.