Combinatorial abstraction refinement for feasibility analysis of static priorities

Combinatorial explosion is a challenge for many analysis problems in the theory of hard real-time systems. One of these problems is static priority schedulability of workload models which are more expressive than the traditional periodic task model. Different classes of directed graphs have been proposed in recent years to model structures like frames, branching and loops. In contrast to dynamic priority schedulers with pseudo-polynomial time analysis methods, static priority schedulability has been shown to be intractable since it is strongly coNP-hard already for the relatively simple class of cyclic digraphs. The core of this problem is the necessity to combine different behaviors of the participating tasks. We introduce a novel iterative approach to efficiently cope with this combinatorial explosion, called combinatorial abstraction refinement. In combination with other techniques it significantly reduces exponential growth of run-time for most inputs. We apply the method to static task priorities and demonstrate that a prototype implementation outperforms the state-of-the art pseudo-polynomial analysis for dynamic priority feasibility. It further shows better scaling behavior for randomly generated problem instances. We extend the approach to non-preemptive schedulers as well as static job-type priorities where jobs of different types in the same task may be assigned different static priorities. Finally, we provide a general, abstract formulation of the algorithm, since we believe that this method can be applicable to a variety of combinatorial problems in the theory of real-time systems with certain abstraction structures.