A stochastic model checking method for the usability of clusters about distributed rendering system

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.