Formally verifying complex real-time systems is a formidable task due
to state-space explosions. We propose a formal framework in which not only
is system concurrency modeled, but scheduling policies are also taken into
consideration for verifying temporal properties. We show how the verification
of concurrent real-time systems, modeled as client-server systems, using the
model-checking approach can benefit from taking advantage of scheduling
policies. Integration of these two concepts, namely scheduling and
model-checking, provides a reduction of the state space when compared to pure
model-checking strategies. Our implementation and experiments corroborate the
feasibility of our approach. Wide-applicability, significant state-space
reduction, and several scheduling semantics are important features of our
framework.