到達目標
(1) 仕様記述とコーディングの違いを理解し，形式仕様記述を実践できる．（定期試験）
(2) 形式手法に基づいた網羅的な検証ツールの動作原理を説明できる．（定期試験）
(3) 産業界での形式手法の活用の可能性について論ずることができる．（定期試験）
ルーブリック
| 理想的な到達レベルの目安 | 標準的な到達レベルの目安 | 未到達レベルの目安 |
| 評価項目1 | 形式仕様記述を実践できる | 仕様記述とコーディングの違いを説明できる | 仕様記述とコーディングの違いが説明できない |
| 評価項目2 | 網羅的な検証ツールの動作原理について，複数の方式を挙げて説明できる | 網羅的な検証ツールの動作原理について，少なくとも一つの方式を挙げて説明できる | 網羅的な検証ツールの動作原理について説明できない |
| 評価項目3 | 産業界での形式手法の活用の可能性について，多面的に論ずることができる | 産業界での形式手法の活用の可能性について，少なくとも一面的に論ずることができる | 産業界での形式手法の活用の可能性について論ずることができない |
学科の到達目標項目との関係
教育方法等
概要:
形式手法はコンピュータ・システムの開発に用いられる手法で，数理論理学に基づいた厳密な意味を持つ仕様記述言語を使って開発要件を表現することにより，設計の上流工程の効率化や網羅的な検証を可能にするものである．本講義では，具体的なツールとしてAlloy Analyzerを用い，実践的な内容を織り交ぜつつ形式手法全般を俯瞰的に学ぶ．
授業の進め方・方法:
教科書を中心として進め，区切り毎に内容のまとめや確認問題を行う．
（再試験について）
総合評価が60 点以上で単位が与えられる．60 点に満たない者に対して一度だけ再試験を実施する．
注意点:
Alloy Analyzerを用いる箇所については実際に自分のパソコンで動かしてみることが望ましい．
授業計画
|
|
週 |
授業内容 |
週ごとの到達目標 |
| 前期 |
| 1stQ |
| 1週 |
1. 論理で考える |
高信頼化の総合技術としての形式手法について，その変遷や言語の分類を以下の項目に沿って学ぶ：
形式手法の既要 /発展の経緯
|
| 2週 |
2. 指先で考える |
軽量形式手法のツールAlloyを実際に動かしつつ，以下の項目に沿って学ぶ：
Alloy入門 / Alloy基礎 / Alloyとその周り
|
| 3週 |
2. 指先で考える |
軽量形式手法のツールAlloyを実際に動かしつつ，以下の項目に沿って学ぶ：
Alloy入門 / Alloy基礎 / Alloyとその周り
|
| 4週 |
3. 機能仕様を論理で考える |
仕様を厳密に表現するために，以下の項目に沿って学ぶ：
手続きとデータ構造 /正しさの基準
|
| 5週 |
3. 機能仕様を論理で考える |
仕様を厳密に表現するために，以下の項目に沿って学ぶ：
手続きとデータ構造 /正しさの基準
|
| 6週 |
4. リファインメントを検査する |
リファインメントの概念について，以下の項目に沿って学ぶ：
リファインメントの基礎
リファインメント検査
|
| 7週 |
4. リファインメントを検査する |
リファインメントの概念について，以下の項目に沿って学ぶ：
リファインメントの基礎
リファインメント検査
|
| 8週 |
5. オブジェクト指向デザインを検査する |
実社会でも多く使われるオブジェクト指向デザインについて形式手法を適用するために，以下の項目に沿って学ぶ：
クラス図とOCL
モデリング言語OCL
オブジェクト指向概念と形式手法
|
| 2ndQ |
| 9週 |
5. オブジェクト指向デザインを検査する |
実社会でも多く使われるオブジェクト指向デザインについて形式手法を適用するために，以下の項目に沿って学ぶ：
クラス図とOCL
モデリング言語OCL
オブジェクト指向概念と形式手法
|
| 10週 |
6. 振る舞い仕様を検査する |
特に組み込みシステムなどで使われる，状態遷移モデルへの形式手法の適用について，以下の項目に沿って学ぶ：
状態遷移システム
時相的な振る舞いの自動解析
|
| 11週 |
6. 振る舞い仕様を検査する |
特に組み込みシステムなどで使われる，状態遷移モデルへの形式手法の適用について，以下の項目に沿って学ぶ：
状態遷移システム
時相的な振る舞いの自動解析
|
| 12週 |
7. プログラム検査を論理で考える |
形式手法を用いてプログラムを検証するということについて，以下の項目に沿って学ぶ：
プログラムの意味
プログラムの検証
テストケースの自動生成
|
| 13週 |
7. プログラム検査を論理で考える |
形式手法を用いてプログラムを検証するということについて，以下の項目に沿って学ぶ：
プログラムの意味
プログラムの検証
テストケースの自動生成
|
| 14週 |
7. プログラム検査を論理で考える |
形式手法を用いてプログラムを検証するということについて，以下の項目に沿って学ぶ：
プログラムの意味
プログラムの検証
テストケースの自動生成
|
| 15週 |
前期末試験 |
|
| 16週 |
前期末試験の解答と解説 |
|
モデルコアカリキュラムの学習内容と到達目標
| 分類 | 分野 | 学習内容 | 学習内容の到達目標 | 到達レベル | 授業週 |
評価割合
| 試験 | 合計 |
| 総合評価割合 | 100 | 100 |
| 基礎的能力 | 100 | 100 |