一句话：将 UE5 Blueprint 游戏逻辑形式化为 NuSMV 模型，自动检测逻辑 bug，并用数据流优化与变量域抽象缩减状态空间。
本文研究如何把模型检测应用于用 Unreal Engine 5 Blueprint 可视化脚本系统（UE5 Blueprint）编写的游戏程序。Blueprint 通过组合各种处理节点以可视化方式描述游戏逻辑，但随着游戏规模增大，导致游戏无法推进的 bug 越来越难以发现和修复。作者采用形式化验证技术——模型检测来自动检测游戏逻辑 bug，将 Blueprint 编写的游戏程序转换为模型检测器 NuSMV 的输入模型，并通过形式化定义各节点的语义实现模型的自动生成。为缓解状态爆炸，论文还提出数据流优化与变量域抽象两种缩减模型状态数的方法。作者将所提方法应用于一个包含典型标志位管理 bug 的 Blueprint，确认 NuSMV 能正确检测出该 bug，并表明优化与抽象可显著减少状态数。
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.
@inproceedings{paperbot7183,
title = {Verifying Game Logic in Unreal Engine 5 Blueprint Visual Scripting System Using Model Checking},
author = {Kazuki Wayama and Tomoyuki Yokogawa and Sousuke Amasaki and Hirohisa Aman and Kazutami Arimoto},
booktitle = {ASE},
year = {2022},
doi = {10.1145/3551349.3560505}
}