WEKO3
アイテム
時間制約をもつゲームスクリプトを対象としたモデル検査手法の提案
https://ipsj.ixsq.nii.ac.jp/records/237375
https://ipsj.ixsq.nii.ac.jp/records/237375e4ae97ba-9404-4735-b7fe-280bef179449
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-SE24217021.pdf (2.4 MB)
2026年7月18日からダウンロード可能です。
|
Copyright (c) 2024 by the Information Processing Society of Japan
|
|
| 非会員：¥660, IPSJ:学会員：¥330, SE:会員：¥0, DLIB:会員：¥0 | ||
| Item type | SIG Technical Reports(1) | |||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2024-07-18 | |||||||||||||||
| タイトル | ||||||||||||||||
| タイトル | 時間制約をもつゲームスクリプトを対象としたモデル検査手法の提案 | |||||||||||||||
| タイトル | ||||||||||||||||
| 言語 | en | |||||||||||||||
| タイトル | Formal Verification for Node-graph Style Game Scripts with Time Constraints Using Model Checking | |||||||||||||||
| 言語 | ||||||||||||||||
| 言語 | jpn | |||||||||||||||
| 資源タイプ | ||||||||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_18gh | |||||||||||||||
| 資源タイプ | technical report | |||||||||||||||
| 著者所属 | ||||||||||||||||
| 岡山県立大学 | ||||||||||||||||
| 著者所属 | ||||||||||||||||
| 岡山県立大学 | ||||||||||||||||
| 著者所属 | ||||||||||||||||
| 岡山県立大学 | ||||||||||||||||
| 著者所属 | ||||||||||||||||
| 愛媛大学 | ||||||||||||||||
| 著者所属 | ||||||||||||||||
| 岡山県立大学 | ||||||||||||||||
| 著者所属(英) | ||||||||||||||||
| en | ||||||||||||||||
| Okayama Prefectural University | ||||||||||||||||
| 著者所属(英) | ||||||||||||||||
| en | ||||||||||||||||
| Okayama Prefectural University | ||||||||||||||||
| 著者所属(英) | ||||||||||||||||
| en | ||||||||||||||||
| Okayama Prefectural University | ||||||||||||||||
| 著者所属(英) | ||||||||||||||||
| en | ||||||||||||||||
| Ehime University | ||||||||||||||||
| 著者所属(英) | ||||||||||||||||
| en | ||||||||||||||||
| Okayama Prefectural University | ||||||||||||||||
| 著者名 |
田中, 琉吾
× 田中, 琉吾
× 横川, 智教
× 天嵜, 聡介
× 阿萬, 裕久
× 有本, 和民
|
|||||||||||||||
| 論文抄録 | ||||||||||||||||
| 内容記述タイプ | Other | |||||||||||||||
| 内容記述 | これまでに我々は，UE5 Blueprint で作成されたゲームプログラムをモデル検査ツール nuXmv の入力モデルに変換し，自動検証を行うための手法を開発してきた．このフレームワークでは，ノードのセマンティクスを形式的に定義することで，モデルの自動生成を実現している．本研究では，この方法を時間制約のあるノードを扱うために拡張する．本研究では，スクリプトの開始時点からの経過時間を表す変数としてのグローバルクロックを新たに定義することで，このようなノードのモデル化を可能とする． | |||||||||||||||
| 書誌レコードID | ||||||||||||||||
| 収録物識別子タイプ | NCID | |||||||||||||||
| 収録物識別子 | AN10112981 | |||||||||||||||
| 書誌情報 |
研究報告ソフトウェア工学（SE） 巻 2024-SE-217, 号 21, p. 1-8, 発行日 2024-07-18 |
|||||||||||||||
| ISSN | ||||||||||||||||
| 収録物識別子タイプ | ISSN | |||||||||||||||
| 収録物識別子 | 2188-8825 | |||||||||||||||
| Notice | ||||||||||||||||
| SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. | ||||||||||||||||
| 出版者 | ||||||||||||||||
| 言語 | ja | |||||||||||||||
| 出版者 | 情報処理学会 | |||||||||||||||
