Spotlight Abstraction in Model Checking Real-Time Task Schedulability

In this paper we present a new abstraction technique for the model-checking of real-time systems with multiple tasks. Our technique enables the automatic and efficient analysis of the schedulability of real-time tasks for both preemptive and non-preemptive scheduling policies. It is based on the spotlight abstraction principle, which is applied to a queue that contains the tasks of the real-time system to be analyzed. This task-queue is partitioned into a so-called 'spotlight' and a 'shade'. Initially the spotlight contains only a small number of tasks which appear at the front of the queue and will be executed in the near future. The initial shade contains the remaining tasks which will be executed only after the spotlight tasks have been processed. On the basis of these assumptions an abstract state space model is generated. In this model the spotlight is considered in detail, whereas the behavior of the shade is almost entirely abstracted away. Such an abstract model is checked iteratively as follows: first the schedulability of the spotlight tasks is analyzed, and the result is saved for later re-use. If this result is still inconclusive, more tasks are brought from the shade into a now "broader" spotlight, with which the model checker can proceed. These steps are repeated until a decisive schedulability result is reached. In this manner we divide the entire model checking problem into smaller sub-problems such that, in the average case, the model checker's run-time is still acceptably short.