Scheduling Overload for Real-Time Systems using SMT Solver

In a real-time system, tasks are required to be completed before their deadlines. Due to heavy workload, the system may be in overload condition under which some tasks may miss their deadlines. To alleviate the degrees of system performance degradation cased by the missed deadline tasks, the design of scheduling is crucial. Many design objectives can be considered. In this paper, we focus on maximizing the total number of tasks that can be completed before their deadlines. A scheduling method based on satisfiability modulo theories (SMT) is proposed. In the method, the problem of scheduling is treated as a satisfiability problem. The key work is to formalize the satisfiability problem using first-order language. After the formalization, a SMT solver (e.g., Z3, Yices) is employed to solver such a satisfiability problem. An optimal schedule can be generated based on a solution model returned by the SMT solver. The correctness of this method and the optimality of the generated schedule are straightforward. The time efficiency of the proposed method is demonstrated through various simulations. To the best of our knowledge, it is the first time introducing SMT to solve overload problem in real-time scheduling domain.