一种对于分布式渲染集群系统可用性分析的概率模型检查方法

摘要

本文通过使用概率模型检查工具PRISM,研究渲染集群节点系统的可用性。针对1个集群节点和2个集群节点组成的系统,使用PRISM模型语言进行了建模,并通过相关属性的描述,从而得到系统可用性的稳态概率分布。%In order to study the usability of rendering clusters,we adopt in a Probabilistic Model checker-PRISM.We formalized a one-node cluster system and a two-node cluster system with PRISM language,and then through the property language and verification method,we get the steady-state probability about the usability.