Hsiung, Pao-AnnPao-AnnHsiungFARN WANGKuo, Yue-SunYue-SunKuo2020-06-042020-06-04199903029743https://www.scopus.com/inward/record.uri?eid=2-s2.0-84948991684&doi=10.1007%2f3-540-49059-0_2&partnerID=40&md5=4167f3c5fdbf2490313a582b67026756A formal framework is proposed for the verification of complex realtime 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. © Springer-Verlag Berlin Heidelberg 1999.Interactive computer systems; Real time systems; Scheduling; Semantics; Client server; Complex real-time systems; Formal framework; Important features; Scheduling semantics; Scheduling systems; State-space reduction; Model checkingconference paper10.1007/3-540-49059-0_22-s2.0-84948991684