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

SMV model checking tool-based modeling and analysis of distributed animation rendering system software

作　　者：洪志国[1] 王永滨[1] 石民勇[1] 于水源[1] HONG Zhiguo;WANG Yongbin;SHI Minyong;YU Shuiyuan(School of Computer Science and Cybersecurity,Communication University of China,Beijing 100024,China)

机构地区：[1]中国传媒大学计算机与网络空间安全学院,北京100024

出　　处：《黑龙江大学自然科学学报》2020年第3期362-366,共5页Journal of Natural Science of Heilongjiang University

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

摘　　要：利用网络资源搭建分布式动漫渲染系统是提升渲染速度、克服动漫制作效率瓶颈的有效方式。分布式动漫渲染系统软件的健壮性和可用性是渲染系统稳定高效运行的重要保障。因此,从模型检测角度对软件开发进行建模与分析将有效地预防和消除程序中的Bugs,保证程序设计的正确性。基于模型检测方法对系统进行了建模,采用计算树逻辑(Computational tree logic,CTL)对系统待验证的性质进行了描述,并进一步通过符号模型检查(Symbolic model verification,SMV)工具验证了所构建模型的相关性质,为提高系统软件开发的正确性提供了重要的理论依据。Utilizing network resources to build distributed animation rendering system is an effective way to improve the rendering speed and overcome the bottleneck of producing animation. The robustness and availability of distributed animation rendering system is an important guarantee for the stable and efficient operation. Therefore, from the perspective of model checking in software development for modeling and analysis, it will effectively prevent and eliminate bugs in the program, ensuring the correctness of programming. Based on model checking method for system modeling, the properties to be verified of system is described using computational tree logic(CTL).Furthermore, the related properties are verified with symbolic model verification(SMV). This methodology offers important theoretical accordance to improve the correctness of software development.

关 键 词：模型检测 动漫渲染 SMV 状态机 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论]