Scheduling System Verification

. 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 statespace 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. 1 Introduction Model-checking has the promise of a formal, full, and automatic verification of complex industrial implementations in the future. In spite of the recent success in the formal verification of real-time systems, it is still quite infeasible to formally verify largescale real-world systems due to their high degree of complexity. On the other hand, engineers have developed various paradigms t..