TY - JOUR
T1 - Towards the Availability of the Distributed Cluster Rendering System: Automatic Modeling and Verification
AU - Wang, Kemin
AU - Jiang, Zhengtao
AU - Wang, Yongbin
AU - Yang, Youshan
AU - Jiang, Wei
PY - 2012
Y1 - 2012
N2 - In this study, we proposed a Continuous Time Markov Chain Model towards the availability of n-node clusters of Distributed Rendering System. It's an infinite one, we formalized it, based on the model, we implemented a software, which can automatically model with PRISM language. With the tool, whenever the number of node-n and related parameters vary, we can create the PRISM model file rapidly and then we can use PRISM model checker to verify ralated system properties. At the end of this study, we analyzed and verified the availability distributions of the Distributed Cluster Rendering System while the node number-n varying under different repair modes.
AB - In this study, we proposed a Continuous Time Markov Chain Model towards the availability of n-node clusters of Distributed Rendering System. It's an infinite one, we formalized it, based on the model, we implemented a software, which can automatically model with PRISM language. With the tool, whenever the number of node-n and related parameters vary, we can create the PRISM model file rapidly and then we can use PRISM model checker to verify ralated system properties. At the end of this study, we analyzed and verified the availability distributions of the Distributed Cluster Rendering System while the node number-n varying under different repair modes.
M3 - Journal article
SN - 2040-7459
VL - 4
SP - 4453
EP - 4457
JO - Research Journal of Applied Science, Engineering and Technology
JF - Research Journal of Applied Science, Engineering and Technology
IS - 21
ER -