| Project/Area Number |
23K11382
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 62040:Entertainment and game informatics-related
|
|---|
| Research Institution | Okayama Prefectural University |
|---|
Principal Investigator |
横川 智教 岡山県立大学, 情報工学部, 准教授 (50382362)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
天嵜 聡介 岡山県立大学, 情報工学部, 准教授 (00434978)
阿萬 裕久 愛媛大学, 総合情報メディアセンター, 教授 (50333513)
|
|---|
| Project Period (FY) |
2023-04-01 – 2026-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| Budget Amount *help |
¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000)
Fiscal Year 2025: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2024: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2023: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
|
|---|
| Keywords | モデル検査 / ビデオゲーム / Unreal Engine / 自動検証 / ビデオゲーム開発 / ノードグラフ |
|---|
| Outline of Research at the Start |
本研究ではビデオゲーム開発の QA/QC プロセスを効率化するため，ノードグラフとして記述されたゲームロジックをモデル検査により自動検証するための枠組みを開発する．具体的には，以下の3つの実現を目指す．
(1) ノードグラフからのモデル作成を自動化するための「ノードセマンティクス」の段階的詳細化技術の開発
(2) ノードグラフの自動検証を高速化するための近似処理に基づくモデルサイズ削減技術の開発
(3) ゲーム開発プロジェクトへの適用実験を通した効果の検証
これにより，モデル検査を用いてゲームロジックのバグを自動的に検出することが可能となり，QA/QC プロセスの大幅な効率化を達成できる．
|
| Outline of Annual Research Achievements |
本研究では，ノードベースのビジュアルスクリプト言語によって記述されたゲームロジック（本研究ではノードグラフと呼ぶ）の不具合を，モデル検査技術によって自動的に検出するための枠組みの開発を目的としている．2023年度は，ノードグラフからモデルを自動的に生成し検証を行うための「ノードセマンティクス」の段階的詳細化技術の開発を行った．
ノードセマンティクスは，ノードグラフを構成するゲーム内変数や条件分岐を表す様々なノードの振る舞いを定式化したものである．モデル検査によりノードグラフの不具合検出を行う上では，ノードセマンティクスの抽象化および詳細化が非常に重要である．ノードグラフの不具合をモデル上で再現するためには，モデルの振る舞いを実装に近づけるべく詳細化が必要となり，短時間で検証を完了するためには探索する状態空間を削減するべく抽象化が必要となる．本年度はノードセマンティクスの詳細化の一環として，時間制約をもつノードグラフのモデル化手法についての開発を行った．特に，ゲーム開発で広く用いられているビジュアルスクリプティングシステムである Unreal Engine 5 Blueprint について，時間制約を実装するためのノードである Delay ノードと Timeline ノードの振る舞いをノードセマンティクスとして定式化する枠組みを開発した．Unreal Engine 5 Blueprint では，時間制約をもたないノードによる処理は同時刻に完了し，時間制約をもつノードについてのみ制約条件を満たす時刻に処理が完了する，という振る舞いをもつ．我々は，ノードグラフに対して，各ノードについて処理を開始した時刻を保存するための変数と，大域的な時刻を表す変数を新たに定義することで，上記の振る舞いのモデル化を行った．以上の成果は1件の国際会議において発表を行っている．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
ノードグラフからモデルを自動的に生成し検証を行うための「ノードセマンティクス」の段階的詳細化技術の開発に関して，時間制約をもつノードグラフのモデル化手法を開発し，例題ノードグラフについて実際にモデル化を行い，モデル検査ツール nuXmv による検証を実行できた．上記については査読付国際会議において発表しており，概ね順調に研究を進めることができているといえる．
|
| Strategy for Future Research Activity |
引き続き，「ノードセマンティクス」の段階的詳細化技術の開発を進めていく．直近の課題として，時間制約を表現するための詳細化に付随して生じる状態爆発問題への対応を行う．時間制約を表すために変数を新たに定義することにより，状態空間が大きくなるため，検証コストが増大することが予想される．そのため，その他の部分に抽象化を施すことで検証コストを抑制する必要があると考えている．
|
