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

作     者：洪志国 王永滨 石民勇 于水源 HONG Zhiguo;WANG Yongbin;SHI Minyong;YU Shuiyuan

作者机构：中国传媒大学计算机与网络空间安全学院北京100024 

基　　金：国家科技支撑计划课题资助项目(2013BAH54F03) 中国传媒大学优秀中青年教师培养工程资助项目(YXJS201508) 中国传媒大学理工科规划项目(3132015XNG1504) 

出 版 物：《黑龙江大学自然科学学报》 (Journal of Natural Science of Heilongjiang University)

年 卷 期：2020年第37卷第3期

页      码：362-366页

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

主 题 词：模型检测 动漫渲染 SMV 状态机 

学科分类：08[工学] 0835[0835] 081202[081202] 0812[工学-测绘类] 

D　O　I：10.13482/j.issn1001-7011.2019.09.042

馆 藏 号：203960357...