Scheduling System Verification

Pao-Ann Hsiung, Farn Wang, and Yue-Sun Kuo,
Institute of Information Science
Academia Sinica, Taipei, Taiwan.
(TACAS'99, March 1999.)


A formal 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.


scheduling algorithms, model-checking, timed automata, client-server systems