モデル検証入門～ツールに振る舞いを検査させる～
受講スキル
ゲームソフトウェアの複雑な動作に対して，テスティングという検証手段だけでは不十分だと何となく感じており，それを補完する技術に興味がある方ならばどなたでも歓迎します．オートマトン等の計算機科学の基礎知識があればより理解が深まりますが，それらを道具として活用する意欲があれば十分です．
セッションの内容
ゲームソフトウェアにおいて，行動選択の履歴や複数プレーヤーの行動により以後の展開が変わる場合や，複数のスレッド，複数のクライアント・サーバが並行動作，相互作用する場合，起きうる様々な状況に対応する複雑な制御が必要となる．そのような複雑な制御において，「ゲームが進行しなくなる」といった不整合がないことを保証する手段として，モデル検査と呼ばれる技術を紹介する．モデル検査においては，期待する（期待しない）性質が成り立つか，ツールに「網羅的に」調べさせることができ，テスティングを補完する技術として注目を集めている．本セッションにおいては，モデル検査の基本的な考え方を示し，ゲーム開発への適用を想定してツールやその適用手法を紹介する．また「性質を保証する」という考え方に関し，モデル検査以外のアプローチについても紹介する．なお，本セッションで紹介する技術のより詳細な情報をWebにおいて公開する．
講演資料
※資料のダウンロードには ログイン が必要です。
講演者プロフィール
プロフィール
2007年 東京大学大学院情報理工学研究科博士課程修了．博士（情報理工学）．
2007年より国立情報学研究所助教．現在に至る．総合研究大学院大学複合科学研究科助教兼任．サービス指向コンピューティング，ソフトウェア工学に関する研究に従事．またGRACEセンターおよびトップエスイープロジェクトに参加し，企業の開発者を対象とした形式手法・ツールの教育・普及活動にも取り組んでいる