loading...
Verification of Concurrent Client-Server Real-Time Scheduling Systems
Hong Kong, China December 13-December 15
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/RTCSA.1999.811234Sixth International Conference on Rea ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Pao-Ann Hsiung, Academia Sinica
Farn Wang, Academia Sinica
Yue-Sun Kuo, Academia Sinica
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.
Index Terms:
concurrent real-time client-server systems, model-checking, automata, scheduling algorithms, state-space reduction, verification
Citation:
Pao-Ann Hsiung, Farn Wang, Yue-Sun Kuo, "Verification of Concurrent Client-Server Real-Time Scheduling Systems," rtcsa, pp.228, Sixth International Conference on Real-Time Computing Systems and Applications (RTCSA'99), 1999
Usage of this product signifies your acceptance of the Terms of Use.