基于SMV模型检测工具的分布式动漫渲染系统软件建模与分析

摘要

利用网络资源搭建分布式动漫渲染系统是提升渲染速度、克服动漫制作效率瓶颈的有效方式.分布式动漫渲染系统软件的健壮性和可用性是渲染系统稳定高效运行的重要保障.因此,从模型检测角度对软件开发进行建模与分析将有效地预防和消除程序中的Bugs,保证程序设计的正确性.基于模型检测方法对系统进行了建模,采用计算树逻辑(Computational tree logic,CTL)对系统待验证的性质进行了描述,并进一步通过符号模型检查(Symbolic model verification,SMV)工具验证了所构建模型的相关性质,为提高系统软件开发的正确性提供了重要的理论依据.