近年ゲームロジック開発や，それらのQAには大きな工数がかかるようになりました．こうした問題を解決する技術の1つとして形式手法・モデル検査があり，これらの技術を用いることでゲームロジックに一定のバグがないことを論理的に検証することができ，生産性を大きく向上させることができます．過去のCEDEC講演をはじめ，ゲーム開発に形式手法・モデル検査を導入する動きはあるものの，実際のゲーム開発に適用できた事例はほとんど聞きません．本セッションでは，FINAL FANTASY XVの開発で使用したLuminous EngineのVisual Scriptを，モデル検査環境の1つであるNuSMVを用いて検証し，いくつかの種類のバグを自動で検出できるようにした取り組みを紹介します．
講演者プロフィール
長谷川 勇
オープンソース開発、ソフトウェアプロダクト開発、エンタープライズシステム開発などの様々な開発を経てゲームプログラマに。株式会社スクウェア・エニックスに入社後は、Luminous Studio、FINAL FANTASY XVの開発に参加し、VFX・UIを担当。株式会社Luminous ProductionsではR&Dを担当。専門は言語処理系。ACM SIGGRAPH Asia 2018 Real Time Live! Chair、情報処理学会ソフトウェア工学研究会運営委員、情報処理教育委員。共著『ゲームエンジニア養成読本』（Software Design plusシリーズ、技術評論社）。
《講演者からのメッセージ》
ハードウェアの進化や様々な要因によりゲーム開発はどんどん複雑・大規模化してきました。モデル検査は銀の弾丸ではありませんし、導入も大変ですが、こうしたやっかいな開発を助けてくれる強力な手法です。本セッションではVisual Scriptへのモデル検査の適用事例や知見を共有しますが、形式手法やモデル検査の適用先は他にもいろいろ考えられますので、今後のゲーム開発改善の一つの可能性として情報交換などできればと思います。
横川 智教
2004年、大阪大学 大学院基礎工学研究科 博士課程を修了。同年、岡山県立大学 情報工学部 助手。2016年、同大学 情報工学部 准教授。博士（工学）。専門分野はモデル検査を用いたソフトウェアシステムの形式的検証。情報処理学会主催のソフトウェアエンジニアリングシンポジウム（2013〜2017）およびウィンターワークショップ（2014〜2018）において、形式手法の情報交換を目的としたセッションを開催。過去の講演として、「形式仕様記述を用いたモデルベースのソフトウェア検証技術」（ベリサーブ アカデミック イニシアティブ 2016）など。
《講演者からのメッセージ》
モデル検査をソフトウェア開発に活用するためには、対象となるシステムの動きをグラフとしてモデル化したり、調べたい性質を特殊な論理で表現したりと越えなければいけないハードルは多いですが、使いこなせばとても強力な技術です。このセッションでは、実際のゲーム開発へとモデル検査を適用した事例を通して、モデル検査の強みや使いこなすための勘所についてお伝えできればと思います。
