| 研究課題/領域番号 |
23K11382
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分62040:エンタテインメントおよびゲーム情報学関連
|
|---|
| 研究機関 | 岡山県立大学 |
|---|
研究代表者 |
横川 智教 岡山県立大学, 情報工学部, 准教授 (50382362)
|
|---|
| 研究分担者 |
天嵜 聡介 岡山県立大学, 情報工学部, 准教授 (00434978)
阿萬 裕久 愛媛大学, 総合情報メディアセンター, 教授 (50333513)
|
|---|
| 研究期間 (年度) |
2023-04-01 – 2026-03-31
|
| 研究課題ステータス |
交付 (2023年度)
|
| 配分額 *注記 |
4,680千円 (直接経費: 3,600千円、間接経費: 1,080千円)
2025年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
2024年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2023年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
|
|---|
| キーワード | モデル検査 / ビデオゲーム / Unreal Engine / 自動検証 / ビデオゲーム開発 / ノードグラフ |
|---|
| 研究開始時の研究の概要 |
本研究ではビデオゲーム開発の QA/QC プロセスを効率化するため，ノードグラフとして記述されたゲームロジックをモデル検査により自動検証するための枠組みを開発する．具体的には，以下の3つの実現を目指す．
(1) ノードグラフからのモデル作成を自動化するための「ノードセマンティクス」の段階的詳細化技術の開発
(2) ノードグラフの自動検証を高速化するための近似処理に基づくモデルサイズ削減技術の開発
(3) ゲーム開発プロジェクトへの適用実験を通した効果の検証
これにより，モデル検査を用いてゲームロジックのバグを自動的に検出することが可能となり，QA/QC プロセスの大幅な効率化を達成できる．
|
| 研究実績の概要 |
本研究では，ノードベースのビジュアルスクリプト言語によって記述されたゲームロジック（本研究ではノードグラフと呼ぶ）の不具合を，モデル検査技術によって自動的に検出するための枠組みの開発を目的としている．2023年度は，ノードグラフからモデルを自動的に生成し検証を行うための「ノードセマンティクス」の段階的詳細化技術の開発を行った．
ノードセマンティクスは，ノードグラフを構成するゲーム内変数や条件分岐を表す様々なノードの振る舞いを定式化したものである．モデル検査によりノードグラフの不具合検出を行う上では，ノードセマンティクスの抽象化および詳細化が非常に重要である．ノードグラフの不具合をモデル上で再現するためには，モデルの振る舞いを実装に近づけるべく詳細化が必要となり，短時間で検証を完了するためには探索する状態空間を削減するべく抽象化が必要となる．本年度はノードセマンティクスの詳細化の一環として，時間制約をもつノードグラフのモデル化手法についての開発を行った．特に，ゲーム開発で広く用いられているビジュアルスクリプティングシステムである Unreal Engine 5 Blueprint について，時間制約を実装するためのノードである Delay ノードと Timeline ノードの振る舞いをノードセマンティクスとして定式化する枠組みを開発した．Unreal Engine 5 Blueprint では，時間制約をもたないノードによる処理は同時刻に完了し，時間制約をもつノードについてのみ制約条件を満たす時刻に処理が完了する，という振る舞いをもつ．我々は，ノードグラフに対して，各ノードについて処理を開始した時刻を保存するための変数と，大域的な時刻を表す変数を新たに定義することで，上記の振る舞いのモデル化を行った．以上の成果は1件の国際会議において発表を行っている．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
ノードグラフからモデルを自動的に生成し検証を行うための「ノードセマンティクス」の段階的詳細化技術の開発に関して，時間制約をもつノードグラフのモデル化手法を開発し，例題ノードグラフについて実際にモデル化を行い，モデル検査ツール nuXmv による検証を実行できた．上記については査読付国際会議において発表しており，概ね順調に研究を進めることができているといえる．
|
| 今後の研究の推進方策 |
引き続き，「ノードセマンティクス」の段階的詳細化技術の開発を進めていく．直近の課題として，時間制約を表現するための詳細化に付随して生じる状態爆発問題への対応を行う．時間制約を表すために変数を新たに定義することにより，状態空間が大きくなるため，検証コストが増大することが予想される．そのため，その他の部分に抽象化を施すことで検証コストを抑制する必要があると考えている．
|
