Model Checking Task Sets with Preemption Thresholds

摘要

Several models have been developed for symbolic schedulability analysis of periodic, preemptive task sets in real-time systems [1, 11]. However, these models cannot be used to analyze task sets with preemption thresholds. In this paper, we present a new model with a two-clocks scheduler that can be used to efficiently analyze periodic task sets with preemption thresholds. The new model can also be used to compute an optimal set of preemption thresholds for a given priority assignment. In particular, it can be used to compute a feasible set of preemption thresholds that are as small as possible.