コースリーダーのインタビューを，こちらでご覧ください．
モデル検査とは
数学に基づいて，ソフトウェアなどのシステムが正しく動作することを検証する技術を，形式手法と呼びます．モデル検査は，(トップエスイーの別コースである形式仕様記述とともに) 形式手法の代表的な分野のひとつです． 一言で言ってしまうと，モデル検査とは，「あらゆる組み合わせを全部調べ上げて問題がないかどうか調べる」手法です．単純かつ野蛮と思われるかも知れません．しかし実際には，この単純きわまりない目標を現実的な時間で達成するために，奥の深い理論に基づいたツールと，ノウハウを持った検証者 (明日の皆さんの姿です) が必要になるのです．
「あらゆる組み合わせ」を調べるのが大変になる場面の例として，ホームネットワークにおける予約録画を表した下図をご覧ください．このシステムが常に正しく動作することを保証するために，例えばユーザのボタン操作，タイマーの入り/切り，ディスクフル など事象を考慮に入れなければなりません．このような要素をもれなく数え上げることは，おそらく不可能ではないでしょう．しかし，各々がどのタイミングでも，また任意の順序で起こりえる．そのうちの複数が同時に起こることもある，という状況で，すべての可能性を漏れなくテストすることは，現実的には非常に困難です．このような時，「あらゆる組み合わせ」を網羅してくれるモデル検査手法が力を発揮するのです．
本コースで習得する技術
上述のような能力を持つモデル検査器ですが，そのパワーをきちんと生かすには，正しいモデル化が必須です．つまり、モデル検査ツールを使いこなすためには、ソフトウェアエンジニアの重要な能力であるモデル化能力や、問題領域をとらえ、解決手段を発見する能力が必要となるのです． モデル検査コースでは、ソフトウェアの振る舞いをどうモデル化し、検証するかについて学習します。モデル化には、検証する性質に応じて、UMLのステートチャートやタイミング図、CSPなどの並行プロセス記述を用います。単にモデル検査ツールの使い方を学ぶのではなく、ツールを通してエンジニアのモデル能力を育てることを目的としています。具体的には、UMLなどで記述した設計モデルを、検査したい項目から、その構造やデータ、制御フローに着目した検証部分の切り出しや抽象化の方法も学びます。このような検証部分の切り出しや抽象化は、検証のための時間やメモリを大幅に軽減し、状態爆発による検証不能を避けるために重要な作業です。 
さらに、モデル検査では、取りうる状態を網羅するために外部環境を含め全ての状況(閉じたモデル)を規定する必要があります。検査したい項目から、このようなモデルの作成や検証する具体的な性質をブレイクダウンする過程を通じて、何を検証したいのかという問題領域を正しくとらえる能力や、そのための解決手段を発見する能力を養うのです。そして、検証に必要となる数学的背景知識も単に大学でのオートマトンの授業と異なり、具体的な検証方法との関係とともに工学のための活きたサイエンスとして学びます。 最終的には、各講座を通して、たくさんのツールを使うことで、検証内容に応じたツールの使い分けができるようになります。
本コースで育成する人材
モデル検査コースでは，次のような人材を育成します．
- モデル検査手法の基礎理論に一定の理解があり，個別手法の詳細を理解するための基礎ができている．
- モデル検査手法の長所と限界を理解しており，個別の問題 および 開発プロセスへの適用効果を評価することができる．
- モデル検査を開発プロセスに組み込むためのノウハウを身につけている．
- 代表的なモデル検査ツールの特長を理解し，問題に応じて使い分けることができる．
講義紹介
設計モデル検証 (基礎編)
本講座では，モデル検査器 SPIN を用いた検証を学びます．単に検査器の使い方を勉強するだけではなく，実際のソフトウェア開発プロセスに適用する方法を習得します．全体を通して，ネットワーク家電の制御ソフトウェアを題材とした産業ソフトウェアの設計というテーマのもと，標準のモデル記述言語UMLを全面的に採用していますので，設計プロセスの中にいかに検証を組み込んでいくかが体得できます．
設計モデル検証(応用編)
本講座では，基礎編で学んだ検証技術をベースに，代表的な3つのモデル検査ツールであるSPIN、SMV、およびLTSAを使用して，設計モデルの検証手法を実際のシステム開発に適用する方法を習得します．モデル検査技術は進歩が早く，より高機能・高性能な新しいツールがでてきます．これらのツールから最適なものを選択したり，新しいツールへの移行を円滑に行うのは容易ではありません．本講座の例題演習におけるグループ討議を通してモデル検査技術の理解を深め，実用的ノウハウを体得することによって，これらの困難を克服することが期待されます．
並行システムの検証と実装
- 講師: 磯部 祥尚
- 15コマ，2単位
- 開講: 3学期(2011年度)
本講座では，並行システムをモデル化して検証するだけでなく，そのモデルを実装して並列・分散実行する方法についても学ぶことができます．ここで，並行システムの検証にはモデル検査器FDR，実装にはJavaライブラリJCSPを使用します．これらは共にプロセス代数CSPに基づくツールです．プロセス代数は並行システムをモデル化し，解析するための理論です．この講義の特徴は，モデル化（CSP）→検証（FDR)→実装（JCSP）の流れを重視した講義構成にあります．すなわち，検証済のモデルを実装することによって，信頼性の高い並行システムを構築することができます．尚，JCSP（Java用）の他にもCSPモデルを実装するためのライブラリ（C++用，Haskell用，Python用など）やプログラミング言語（GoogleのGo言語など）が公開されており，本講座で習得できる検証や実装の方法は他のプログラミング言語にも有効です．
実装モデル検証
- 講師: 田辺良則，Cyrille Artho
- 15コマ，2単位
- 開講: 3学期(2011年度)
本講座では，代表的ソフトウェアモデル検査器の一つである，Java PathFinder を用いたモデル検査手法を学びます．ソフトウェアモデル検査は，プログラムそれ自体を状態遷移系と見なしてモデル検査する比較的新しい手法です．マルチスレッドプログラムにおける競合条件で発現するような非常に検出しにくいバグを発見することができます．ネットワークプログラムのバグを検出するための最新の手法についても学びます．
性能モデル検証
本講座では，時間オートマトンに基づいたモデル検査ツール UPPAAL を用いて，性能などの時間に関する性質をモデル検査で検証する方法を学びます．時間が関係する性質をモデル検査の手法で検証するためには，通常とは異なった方法が必要となります．本講座では，設計に用いられている UML のモデルとUPPAAL モデルの違いを明確にすることで，実用上必要となる正確なモデルの作成能力を養成します．また，UPPAALモデルを作成する演習を通じて時間に関する検証を体験し，ノウハウや他のモデル検査ツールとの相違を学びます．
モデル検査事例演習 (仮称)
本講義は，2012年度より開講する予定です． 講義名，講師，開講時期，講義内容は変更になることがあります．
- 講師: 早水 公二 (予定)
- 15コマ，2単位
- 開講: 2012年度予定
本講座では，モデル検査の実務を想定し，その開始から終了までの全プロセスを意識した演習を行います．通常，検証作業で体験する，検証対象ソフトウェアの開発者からのヒアリング，ソフトウェアのモデル化，モデル検査，結果報告，そして最終報告書の執筆に至るまで，各フェーズでのポイントを押さえた演習に取り組んでいただきます．モデル検査ツールはSMVを使用します．
修了制作例
モデル検査に関連する修了制作は，毎年行われていますが，最近の修了制作から事例を紹介します．
Promelaコード生成およびエラー原因推定アルゴリズム開発
5期生の佐々木隆益さんの修了制作です． この修了制作では，モデル検査の効率的な実施を課題に上げました．特に，モデルを記述するために Promela という普通の技術者にはなじみの無い言語を用いる点，および，モデル検査器が報告するエラーの情報からその原因を特定するのに工数を要する点の2点を改善することを目標にしています．これを実現するために，技術者にとってよりなじみ深いUMLプロファイルからのPromelaモデル自動生成，および，エラー原因を体系的に特定するための決定木を開発しました．これらの工夫によって，モデル検査に要する工数が短縮される効果が得られました． 
この修了制作は，第5期の優秀賞に選ばれました．