Model Checking of Software Development in Distributed Animation Rendering System

DOI

10.2991/nceece-15.2016.284How to use a DOI?

Keywords

model checking; animation rendering; SMV; the state machine

Abstract

Distributed animation rendering systems are used to speed up of rendering i.e the computational-intensive phase of producing animation. How to develop softwares with high availability and efficiency is a hot topic in distributed animation rendering systems. In this paper, based on model checking method for system modeling, three modules (i.e. rendering management server, rendering nodes and storage system) are modeled and analyzed. Firstly, by analyzing the system’s typical infrastructure, messages-driven finite state machines of such three modules are studied. Then, the properties of such three modules are described using CTL(Computational Tree Logic). Furthermore, safety and livenesses are verified with SMV (Symbolic Model Verification). The methodology of this paper offers important theoretical guide to software development.

Copyright

© 2016, the Authors. Published by Atlantis Press.

Open Access

This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)

TY  - CONF
AU  - ZhiGuo Hong
AU  - Yongbin Wang
AU  - Minyong Shi
PY  - 2015/12
DA  - 2015/12
TI  - Model Checking of Software Development in Distributed Animation Rendering System
BT  - Proceedings of the 2015 4th National Conference on Electrical, Electronics and Computer Engineering
PB  - Atlantis Press
SP  - 1575
EP  - 1579
SN  - 2352-5401
UR  - https://doi.org/10.2991/nceece-15.2016.284
DO  - 10.2991/nceece-15.2016.284
ID  - Hong2015/12
ER  -