Visual script languages with a node-based interface have commonly been used in the video game industry. We examined the bug database obtained in the development of FINAL FANTASY XV (FFXV), and noticed that several types of bugs were caused by simple mis-descriptions of visual scripts and could therefore be mechanically detected. We propose a method for the automatic verification of visual scripts in order to improve productivity of video game development. Our method can automatically detect those bugs by using symbolic model checking. We show a translation algorithm which can automatically convert a visual script to an input model for NuSMV that is an implementation of symbolic model checking. For a preliminary evaluation, we applied our method to visual scripts used in the production for FFXV. The evaluation results demonstrate that our method can detect bugs of scripts and works well in a reasonable time.

Model checking is a technique that can make a verification for finite state systems absolutely automatic. We propose a method for automatic verification of fault-tolerant concurrent systems using this technique. Unlike other related work, which is tailored to specific systems, we are aimed at providing an approach that can be used to verify various kinds of systems against fault tolerance. The main obstacle in model checking is state explosion. To avoid the problem, we design this method so that it can use a symbolic model checking tool called SMV (Symbolic Model Verifier). Symbolic model checking can overcome the problem by expressing the state space and the transition relation by Boolean functions. Assuming that a system to be verified is modeled as a guarded command program, we design a modeling language and propose a translation method from the modeling language to the input language of SMV. We show the results of applying the proposed method to various examples to demonstrate the feasibility of the method.

This paper describes an efficient symbolic model checking algorithm for verification of deadlock free property of high level robot control program called Task Control Architecture (TCA). TCA is a model of concurrent robot control processes. The verification tool we used is the Symbolic Model Verifier (SMV). Since the SMV is not so efficient for verification of liveness properties of many concurrent processes such as deadlock free property, we first described the deadlock free property by using safety properties that SMV can verify efficiently. In addition, we modify the symbolic model checking algorithm of the SMV so that it can handle many concurrent processes efficiently. Experimental measurements show that we can obtain more than 1000 times speed-up by these methods.

There are two approaches for formal verification of sequential designs or finite state machines: language containment checking and symbolic model checking. To verify designs of practical size, in these two approaches, designs are represented symbolically, in practice, by ordered binary decision diagrams. In the conventional algorithm for language containment checking, finite automata given as specifications are also represented symbolically. This paper proposes a new method, called partially explicit method for checking language containment. By representing states of finite automata given as specifications explicitly, this method can remove redundant computations, and as a result, provide better performance than the conventional method which uses the product machines of designs and specifications. The experimental results show that this approach is effective in checking language containment symbolically.

We present a symbolic language emptiness check algorithm based on forward state traversal. A verification property is given by a set of error traces written in ω-regular expression and is manipulated explicitly as a non-deterministic state transition graph. State space of the design model is implicitly traversed along the explicit graph. This method has a large amount of flexibility for controlling state traversal on the property space. It should become a good framework of incremental or approximate verification of ω-regular properties.

The goal of this paper is to propose a new symbolic model checking approach named time-space modal model checking, which could be applicable to verification of bit-slice microprocessor of infinite bit width and one dimensional systolic array of infinite length. A simple benchmark result shows the effectiveness of the proposed approach.