Title :
A stochastic model checking method for the usability of clusters about distributed rendering system
Author :
Kemin Wang ; Yongbin Wang
Author_Institution :
Dept. of Comput., Commun. Univ. of China, Beijing, China
Abstract :
In order to study the usability of rendering clusters, Continuous Time Markov Chains model is used in this paper. By introducing the probabilistic model checker-PRISM, formalize the whole rending cluster system, and through a series of properties about the system, to analyze and verify the usability of the system. We verify the probability of the system´s usability under different situations, one-node cluster, two-node cluster and with it in different situations, talk about the usability in different situations, through comparisons, we get that our method is very correct and positive.
Keywords :
Markov processes; distributed processing; formal verification; pattern clustering; rendering (computer graphics); PRISM; cluster usability; continuous time Markov chains model; distributed rendering system; probabilistic model checker; stochastic model checking method; Analytical models; Maintenance engineering; Markov processes; Mathematical model; Probabilistic logic; Rendering (computer graphics); Usability; CSL; CTMC; PRISM; Stochastic Model Checking; rendering;
Conference_Titel :
Electronic and Mechanical Engineering and Information Technology (EMEIT), 2011 International Conference on
Conference_Location :
Harbin, Heilongjiang, China
Print_ISBN :
978-1-61284-087-1
DOI :
10.1109/EMEIT.2011.6023217
