文献

J-GLOBAL ID：202402266756755298   整理番号：24A1881377

時間制約をもつゲームスクリプトを対象としたモデル検査手法の提案

Formal Verification for Node-graph Style Game Scripts with Time Constraints Using Model Checking

著者 (5件)： 田中琉吾 (岡山県大) ,  横川智教 (岡山県大) ,  天嵜聡介 (岡山県大) ,  阿萬裕久 (愛媛大) ,  有本和民 (岡山県大)
資料名： 情報処理学会研究報告(Web)  (IPSJ Technical Report (Web))
巻： 2024  号： SE-217  ページ： Vol.2024-SE-217,No.21,1-8 (WEB ONLY)  発行年： 2024年07月18日 
JST資料番号： U0451A  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： これまでに我々は,UE5Blueprintで作成されたゲームプログラムをモデル検査ツールnuXmvの入力モデルに変換し,自動検証を行うための手法を開発してきた.このフレームワークでは,ノードのセマンティクスを形式的に定義することで,モデルの自動生成を実現している.本研究では,この方法を時間制約のあるノードを扱うために拡張する.本研究では,スクリプトの開始時点からの経過時間を表す変数としてのグローバルクロックを新たに定義することで,このようなノードのモデル化を可能とする.(著者抄録)

シソーラス用語： *ビデオゲーム ,  *計算機プログラム ,  *モデル検査 ,  節点 ,  意味論 ,  検証 ,  組合せ問題 ,  モデリング ,  制約条件 ,  時間制約 ,  状態爆発問題 ,  ネットワークノード
準シソーラス用語： システム検証 ,  *スクリプト ,  セマンティックス ,  ノード ,  プログラム開発 ,  モデル化

分類 (2件)： 計算機システム開発  (JD02010R) ,  図形・画像処理一般  (JE04010I)

タイトルに関連する用語 (6件)： 制約 ,  ゲーム ,  スクリプト ,  モデル検査 ,  手法 ,  提案