Combinatorial Abstraction Refinement for Feasibility Analysis

The traditional periodic workload model for hard real-time systems has been extended by more expressive models in recent years. These models based on different classes of directed graphs allow modeling of structures like frames, branching and loops. With more expressiveness comes higher complexity of the associated analysis problems. Feasibility of digraph-based models with dynamic priority schedulers has been shown to be tractable via pseudo-polynomial algorithms. However, the problem was shown to be intractable for static priority scheduling since it is strongly coNP-hard already for the relatively simple class of cyclic digraphs. The core of this problem is an inherent combinatorial explosion caused by combining different behaviors of the participating tasks, lacking local worst cases. 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. A prototype implementation for analysing static priority feasibility outperforms the state-of-the art pseudo-polynomial analysis for dynamic priority feasibility. It further shows better scaling behavior for typical problem sizes. 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.