An Improved SMT-Based Scheduling for Overloaded Real-Time Systems

In real-time systems, completing tasks by their deadlines is as significant as getting the correct results for tasks. Once the workload exceeds the system capacity, it is difficult to complete all tasks correctly before the deadlines. As a result, some tasks will miss the deadlines, leading to system performance degradation or security issues. To alleviate system performance degradation caused by overload, Cheng et al. proposed an SMT-based scheduling algorithm, finding that a SMT solver is an efficient tool to solve the scheduling problem in overloaded real-time systems. However, we notice that their method has a large amount of redundant encoding. Moreover, the SMT solver must be called in a loop to calculate the optimal solution, which increases the computational cost and reduces the efficiency. This paper improves the method proposed by Cheng et al. by eliminating redundant encoding and successive calls of the SMT solver, thus making the SMT-based algorithm more compact and productive. The experimental results show that the updated SMT-based method can significantly improve the system performance.