Verification of Concurrent Client-Server Real-Time Scheduling Systems

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


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.


concurrent real-time client-server systems, model-checking, automata, scheduling algorithms, state-space reduction, verification