コースリーダーのインタビューを，こちらでご覧ください．
形式仕様記述コース
形式仕様記述コースで習得する技術
本コースでは，ソフトウェア開発の上流において開発対象を表現した成果物，特に機能仕様の，形式仕様言語を用いたモデル化と検証のための技術を学びます．ここで形式仕様言語とは，厳密な文法・意味論を持つ言語であり，「何をするシステムを作るのか」を抽象的に，すなわち「どう作るか」を捨象した形で記述するのに適したものです．本コースで学ぶ技術においては，機能仕様をはじめとした上流の成果物における品質向上を行うことによる開発の効率化と安定化，特に下流での誤りの発見・修正の際に生じる大きな手戻りコストの防止を目指します．加えて，下流の最終的な成果物であるプログラムを，効率的に，信頼できる形で得るための技術も扱います．
形式仕様記述の効果としては第一に，厳密な記述を行う過程において，思い込みや誤解の原因となる曖昧さを排除することができます．形式仕様言語を用いた際には一定のルールに基づき記述を行うため，対象システムへの理解を深めながら，一意に意味が定まる明確な記述を行うことになるからです．ここで，「厳密に」とは「詳細に」ということではありません．その記述を行う時点で決められない・決めたくない実装詳細に対しては，多くの場合最低限の制約を与えるなど，抽象的な定義を行うことができるにようになっています．
第二に，厳密な記述を行うことにより，特にツールを用いての科学的・系統的な検証の可能性が大きく広がります．簡単なところでは，例えば未定義の型の利用などを検出する型チェックを自動的に行うことが考えられます．さらには，実行（シミュレーション）・テストによる動作確認，証明やモデル検査といった高い信頼性を保証する検証手段まで，様々な分析が可能になります．
本コースではこれらの効果を得るための原則と基礎技術，例えば「ソフトウェアシステム・プログラムの正しさは，どのような観点から，どのように厳密に表現するか」といったことを，代表的な形式仕様言語とその支援ツールの活用を通して学びます．これらの言語・ツールは数理論理学に基づいていますが，その基礎理論を踏まえつつ，それらをどのように工学的に活用していくかを学んでいきます．
ここで，対象となるシステムの性質や開発の進め方は組織・プロジェクトによって多種多様であり，それぞれの抱える課題も異なります．それに応じて，形式仕様言語やそれを用いた検証方法（ツール機能）の使い方も様々です．このため，本コースでは複数の手法・ツールを学ぶことによって，上記に挙げたような共通の原則と基礎技術を身につけるとともに，課題に応じた解決アプローチの選択・適用を行う力を身につけることを目指します．
形式仕様記述コースで育成する人材
- 個々の形式仕様言語による記述を行うための基礎として，ソフトウェアシステムの機能を，数理論理学に基づき厳密に抽象モデル化するための考え方を身につけている．
- 個々のツールによる検証を行うための基礎として，ソフトウェアシステム・プログラムに対する正当性の基準を厳密に制約式として定め，その成否について論理的に検討する考え方を身につけている．
- 解決すべき問題に対して，モデル化および検証に対する様々なアプローチの特徴を考慮，検討して，アプローチを選択することができる．
- 形式記述・形式検証の利点と限界点を把握し，その効果について客観的に議論，評価することができる．
講義紹介
形式仕様記述（基礎・VDM編）
- 講師: 石川 冬樹
- 単位: 2
- 開講学期: 2学期
比較的馴染みやすい手法であるVDMを題材として，形式仕様記述におけるモデル化・記述と分析・検証の基礎を学びます．またVDMの実習体験を基に，形式仕様記述における他の手法・ツールのアプローチや，自然言語や図表との関連についても俯瞰的に議論します．
形式仕様記述（Bメソッド編）
- 講師: 來間 啓伸
- 単位: 2
- 開講学期: 3学期
信頼性の高いシステムを効率よく開発するための手法であるBメソッドについて学びます．これにより，証明と段階的詳細化により，仕様に対して正しいことがすでに保証されたコードを生成するための考え方を身につけます．
プログラム解析
- 講師: 橋本 祐介
- 15コマ，2単位
- 開講学期: 2学期（2011年度）
プログラムに対して直接形式仕様の考え方を活用し，厳密な仕様記述を行うとともに検証を行う方法，そのノウハウを学びます．具体的にはJavaプログラムを対象とし，JMLによる仕様記述と，それを活用した単体テストや静的検証を実際のツール利用を通して学びます．
形式仕様記述（セキュリティ編）
- 講師: 來間 啓伸，粂野 文洋
- 15コマ，2単位
- 開講学期: 4学期（2011年度）
アクセス制御の問題を共通題材とし，段階的詳細化，定理証明，モデル検査と異なる性質を持つ手法・ツールを用いて取り組みます．この取り組みを通し，セキュリティに対する問題についての様々なアプローチの利点や限界について議論します．
形式仕様記述（実践編） (仮称)
本講義は，2012年度より開講する予定です． 講義名，講師，開講時期，講義内容などは変更になることがあります．
- 講師: 石川 冬樹（その他外部講師）
- 単位: 7コマ，1単位
- 開講学期: 3学期（2012年度・予定）
他講義で扱ったものに限らず，形式手法における様々な手法・ツールの俯瞰と比較を通し，共通の考え方・原則を確認するとともに，異なる活用のアプローチを議論します．また代表的な事例や，事例調査報告，適用ガイダンスなどの解説を通し，実際に活用するための課題や検討事項，工夫などについて議論します．
定理証明と検証 (仮称)
本講義は，2012年度より開講する予定です． 講義名，講師，開講時期，講義内容などは変更になることがあります．
- 講師: 今井宜洋(予定)
- 8コマ，1単位
形式手法によるシステムの検証手法のなかに，定理証明に基づいたものがあります．これは，システムを数学的対象としてモデル化した上で，システムが満たすべき性質を定理として述べ，その証明を行うことで検証を行うものです．本講義では，代表的な定理証明支援ツールのうちの一つである Coq を取り上げ，その基本的な使用法と，ソフトウェア検証への応用を学びます．講師は実際に業務でこの手法を適用しており，講義中では事例の紹介も行います．
修了制作例
DSLによる設計情報記述に対する誤り検出方法の考察
5期生・佐々木高洋さんの修了制作です． プログラム検証の基礎理論を踏まえ，業務で用いているDSL（Domain Specific Language）における入力チェックの十分性判定や，十分でない場合の反例出力のための仕組みを構築しました．
要求仕様の精度向上の試み〜シミュレーション投入システムへの適用
2期生・井上拓さんの修了制作です． 一般的なレビューや形式仕様記述による検証などを段階的に利用する疑似プロジェクトを立ち上げ，個々の手法によりどのように品質向上（修正）が行われたかを評価し，それら手法の利用効果について考察しました．