A theoretical framework is proposed for the verification of complex
real-time systems, modeled as client-server scheduling systems,
using the popular model-checking approach. Model-checking is often
restricted by the large state-space of complex real-time systems.
The scheduling of tasks in such systems can be taken advantage of
for model-checking. Our implementation and experiments corroborate
the feasibility of such an approach. Wide-applicability,
significant state-space reduction, and several scheduling semantics
are some of the important features in our theory and implementation.