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

A Stochastic Model Checking Method for the Usability of Clusters about Distributed Rendering System

作　　者：王克敏[1] 王永滨[1] 

机构地区：[1]中国传媒大学计算机学院,北京100024

出　　处：《中国传媒大学学报（自然科学版）》2011年第3期34-39,共6页Journal of Communication University of China：Science and Technology

摘　　要：本文通过使用概率模型检查工具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.

关 键 词：概率模型检查 渲染集群 PRISM CTMC CSL 

分 类 号：TP301.6[自动化与计算机技术—计算机系统结构]