タグ：
日時：
2013年08月21日(水)14時50分〜15時50分
形式： セッション(60分)
受講スキル：
大学教養レベルの論理学。ノベルゲームなどのスクリプトが書ける程度のゲーム開発経験。
受講者が得られるであろう知見:
ゲームシナリオ進行に関してモデル検査を使うための具体的なノウハウ。ゲーム開発にモデル検査を導入するためのヒント。
セッションの内容
仕様の通りに正しく振る舞うソフトウェアを開発するのは極めて困難であるが、ソフトウェア工学において検討されてきた「モデル検査」は、ソフトウェアをモデル化し、その振る舞いを網羅的に検証することで、仕様の通りに正しく振る舞うソフトウェアの開発を支援する。
コンピュータゲームにおけるシナリオ進行は、状態遷移に基づくスクリプト表現（DSL）で記述されることが多く、モデル検査を行うためのモデル表現と親和性が高い。
本講演では、簡単なノベルゲームエンジンを示し、その上に記述されたゲームのシナリオ進行を、モデル検査によって検証できることを示す。
講演者プロフィール
長久勝
所属 ： 国立情報学研究所
役職 ： GRACEセンター/先端ICTセンター<br>特任技術専門員
ゲーム、映像配信の技術職を経て現職。ソフトウェア工学教育と、学術クラウドに携わっている。早稲田大学MNC非常勤講師兼務。NADEC主宰、ゲームコミュニティサミット2013実行委員、IGDA日本福島ゲームジャムT/F副世話人。単著「Javaゲームプログラミングアルゴリズムとフレームワーク」、雑誌特集「生物の生きるしくみを応用する免疫アルゴリズム」、TopSE修了制作「FDRによるRPGシナリオの検証」、共著「ゲームクリエイターが知るべき97のこと」。CEDECでは、2005-2011「ゲームAI RT」、CEDECラボ2008プログラム委員、2009講演「僕より賢いSATソルバー」。
