@techreport{oai:ipsj.ixsq.nii.ac.jp:02007718,
 author = {茅野,立 and 横川,智教 and 須田,元太郎 and 天嵜,聡介 and 阿萬,裕久 and 有本,和民},
 issue = {18},
 month = {Mar},
 note = {本研究では，UE5 Blueprintで記述されたゲームロジックにモデル検査を適用するため，ノードグラフをSMVプログラムへ自動変換する変換器を提案・実装した．ノードグラフから得られるテキストダンプ（ノードテキスト）から抽出したメタ情報と，ノード種別ごとのセマンティクス定義を入力として，実行フローとデータフローを遷移として表現することでSMVプログラムとしてのモデル化を行う．特に，ノードセマンティクスをJSONとして外部化し，ノードの追加・変更をプログラム本体から分離することで拡張性を高め，検証上重要でないノードは実行フローのみに着目して抽象化を行った．開発したツールの有効性を確認するため，変換器を用いて典型的なバグをもつノードグラフからSMVプログラムを生成し，モデル検査ツールNuSMVによる検証を行った．その結果，バグを検出するとともに反例トレースが得られ，自動生成したモデルが正しくバグを検出できることを確認した．, In this study, we proposed and implemented a converter that automatically transforms node graphs into SMV programs to apply model checking to game logic written in UE5 Blueprints. The converter models the logic as an SMV program by representing execution and data flows as transitions, using meta-information extracted from text dumps (node text) of node graphs and semantic definitions for each node type as inputs. In particular, we enhanced extensibility by externalizing node semantics as JSON files, separating node additions and modifications from the main program. Additionally, nodes that are not critical for verification were abstracted by focusing solely on their execution flow. To confirm the effectiveness of the developed tool, we generated SMV programs from node graphs containing typical bugs using the converter and performed verification with the model checking tool NuSMV. As a result, we successfully detected the bugs and obtained counterexample traces, confirming that the automatically generated models can correctly identify defects.},
 title = {UE5 Blueprintのゲームスクリプトを対象としたモデル検査による自動検証環境の開発},
 year = {2026}
}