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 three-valued spotlight abstraction, 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 that 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, whereby a third truth value “u” (unknown) is used to logically indicate the loss of information which the abstraction of the shade entails. 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.