| 研究課題/領域番号 |
23K11382
|
|---|
| 研究機関 | 岡山県立大学 |
|---|
研究代表者 |
横川 智教 岡山県立大学, 情報工学部, 准教授 (50382362)
|
|---|
| 研究分担者 |
天嵜 聡介 岡山県立大学, 情報工学部, 准教授 (00434978)
阿萬 裕久 愛媛大学, 総合情報メディアセンター, 教授 (50333513)
|
|---|
| 研究期間 (年度) |
2023-04-01 – 2026-03-31
|
| キーワード | モデル検査 / ビデオゲーム / Unreal Engine / 自動検証 |
|---|
| 研究実績の概要 |
本研究では，ノードベースのビジュアルスクリプト言語によって記述されたゲームロジック（本研究ではノードグラフと呼ぶ）の不具合を，モデル検査技術によって自動的に検出するための枠組みの開発を目的としている．2023年度は，ノードグラフからモデルを自動的に生成し検証を行うための「ノードセマンティクス」の段階的詳細化技術の開発を行った．
ノードセマンティクスは，ノードグラフを構成するゲーム内変数や条件分岐を表す様々なノードの振る舞いを定式化したものである．モデル検査によりノードグラフの不具合検出を行う上では，ノードセマンティクスの抽象化および詳細化が非常に重要である．ノードグラフの不具合をモデル上で再現するためには，モデルの振る舞いを実装に近づけるべく詳細化が必要となり，短時間で検証を完了するためには探索する状態空間を削減するべく抽象化が必要となる．本年度はノードセマンティクスの詳細化の一環として，時間制約をもつノードグラフのモデル化手法についての開発を行った．特に，ゲーム開発で広く用いられているビジュアルスクリプティングシステムである Unreal Engine 5 Blueprint について，時間制約を実装するためのノードである Delay ノードと Timeline ノードの振る舞いをノードセマンティクスとして定式化する枠組みを開発した．Unreal Engine 5 Blueprint では，時間制約をもたないノードによる処理は同時刻に完了し，時間制約をもつノードについてのみ制約条件を満たす時刻に処理が完了する，という振る舞いをもつ．我々は，ノードグラフに対して，各ノードについて処理を開始した時刻を保存するための変数と，大域的な時刻を表す変数を新たに定義することで，上記の振る舞いのモデル化を行った．以上の成果は1件の国際会議において発表を行っている．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
ノードグラフからモデルを自動的に生成し検証を行うための「ノードセマンティクス」の段階的詳細化技術の開発に関して，時間制約をもつノードグラフのモデル化手法を開発し，例題ノードグラフについて実際にモデル化を行い，モデル検査ツール nuXmv による検証を実行できた．上記については査読付国際会議において発表しており，概ね順調に研究を進めることができているといえる．
|
| 今後の研究の推進方策 |
引き続き，「ノードセマンティクス」の段階的詳細化技術の開発を進めていく．直近の課題として，時間制約を表現するための詳細化に付随して生じる状態爆発問題への対応を行う．時間制約を表すために変数を新たに定義することにより，状態空間が大きくなるため，検証コストが増大することが予想される．そのため，その他の部分に抽象化を施すことで検証コストを抑制する必要があると考えている．
|
| 次年度使用額が生じた理由 |
（理由）ツール開発および実験のための計算機の購入を計画していたが，昨今の円安による計算機の価格高騰により，必要な性能と価格とのバランスを再検討する必要が出てきたため当該年度では購入を控えた．
（使用計画）状況を踏まえつつ，性能と価格のバランスを検討し適宜購入する計算機を決定する．
|
