@techreport{oai:ipsj.ixsq.nii.ac.jp:00237375,
 author = {田中, 琉吾 and 横川, 智教 and 天嵜, 聡介 and 阿萬, 裕久 and 有本, 和民},
 issue = {21},
 month = {Jul},
 note = {これまでに我々は，UE5 Blueprint で作成されたゲームプログラムをモデル検査ツール nuXmv の入力モデルに変換し，自動検証を行うための手法を開発してきた．このフレームワークでは，ノードのセマンティクスを形式的に定義することで，モデルの自動生成を実現している．本研究では，この方法を時間制約のあるノードを扱うために拡張する．本研究では，スクリプトの開始時点からの経過時間を表す変数としてのグローバルクロックを新たに定義することで，このようなノードのモデル化を可能とする．},
 title = {時間制約をもつゲームスクリプトを対象としたモデル検査手法の提案},
 year = {2024}
}