Abstract
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.