Verifying Game Logic in Unreal Engine 5 Blueprint Visual Scripting System Using Model Checking

This paper examines modeling methods for applying model checking to game programs created with Unreal Engine 5 Blueprint scripting system (hereinafter UE5 Blueprint). UE5 Blueprint can visually describe game logic by combining various processing nodes, but as the size of the game grows, it becomes more difficult to find and fix bugs that prevent the game from progressing. In this paper, a formal verification technique, model checking, is used to automatically detect game logic bugs. We convert a game program created in UE5 Blueprint into an input model for the model-checker NuSMV to achieve verification by NuSMV. The proposed framework enables the automatic generation of models by formally defining the semantics of nodes. We also propose methods for data flow optimization and abstraction of variable domain for the purpose of reducing the number of states in the model. We applied the proposed method to a blueprint containing a typical flag management bug and confirmed that the bug was correctly detected by NuSMV. Furthermore, we show that the number of states can be significantly reduced by the optimization and abstraction.