ソフトウェア検証

科目基礎情報

学校 仙台高等専門学校 開講年度 令和02年度 (2020年度)
授業科目 ソフトウェア検証
科目番号 0107 科目区分 専門 / 選択
授業形態 講義 単位の種別と単位数 学修単位: 2
開設学科 情報システム工学科 対象学年 5
開設期 前期 週時間数 2
教科書/教材 「形式手法入門」中島震 (オーム社)
担当教員 岡本 圭史

到達目標

・ソフトウェア検証の一手法である形式手法の基本的概念を理解できる。
・Alloyの基礎的な文法及び解析法を理解し,それを用いて基礎的な事例を解析できる。

ルーブリック

理想的な到達レベルの目安標準的な到達レベルの目安最低限レベルの目安(可)未到達レベルの目安
ソフトウェ検証の一手法である形式手法の概念に関する理解形式手法の概念が理解でき,それを応用した解析が可能である。形式手法の概念が理解でき,それを用いた基礎的な解析が可能である。形式手法の概念が理解できる。形式手法の概念が理解できない。
Alloyに関する理解Alloyの基礎的な文法及び解析法を理解し,それを応用した事例解析ができる。Alloyの基礎的な文法及び解析法を理解し,それを用いて基礎的な事例を解析できる。Alloyの基礎的な文法及び解析法を理解できる。Alloyの基礎的な文法及び解析法を理解できない。

学科の到達目標項目との関係

教育方法等

概要:
ソフトウェアを正しく構築するために必須であるソフトウェア検証に関し,ソフトウェア検証で用いられる手法の一つである形式手法をAlloyを用いて修得する。ソフトウェアの正しさに関する様々な概念を学び,正しさの解析をAlloyを用いて演習する。
授業の進め方・方法:
教科書及びパワーポイントスライドを用いて関連知識の習得し,修得した知識を基にAlloyツールを用いて演習する。
注意点:
・演習にはAlloyツールを用いるため,Alloyツールの実行環境が必要である。
・演習にあたっては,授業時間の他にも,昼休みや放課後を利用して自主的に行うことが望まれる。
・理論的背景として情報数学の知識が使われるため,情報数学に関する科目を受講していることが望ましい。

授業計画

授業内容 週ごとの到達目標
前期
1stQ
1週 ガイダンス,環境構築 Alloyの実行環境を構築し,簡単な例題を実行できる。
2週 Alloy文法 Alloyの簡単な文法を理解し,簡単な例題を記述できる。
3週 Alloy解析 Alloyの関連な例題を解析できる。
4週 Compositeパターン Compositeパターンを理解し,それを用いた簡単な例題を記述できる。
5週 抽象データの表現と解析 抽象データの表現を理解し,それを用いた簡単な例題を解析できる。
6週 機能仕様の表現と解析 機能仕様の表現を理解し,それを用いた簡単な例題を解析できる。
7週 Alloy入門のまとめ 抽象データの表現と機能仕様の表現を用いて,例題を表現・解析できる。
8週 Alloyを用いた解析1 Alloyを用いて,具体的な事例を記述し,解析できる。
2ndQ
9週 Alloyを用いた解析2 Alloyを用いて,具体的な事例を記述し,解析できる。
10週 Alloyの基礎 Alloyの基礎理論を理解し,解析に活用できる。(37ページのスコープを増やす例)
11週 手続きとデータ構造 手続きとデータ構造を理解し,Alloyを用いて記述できる。
12週 正しさの基準 正しさの基準を理解し,Alloyを用いて記述できる。
13週 リファインメントの基礎 リファインメント関係を理解し,Alloyを用いて記述できる。
14週 リファインメント検査 リファインメント検査を理解し,Alloyを用いて解析できる。
15週 期末試験 期末試験の解説を行う。
16週

モデルコアカリキュラムの学習内容と到達目標

分類分野学習内容学習内容の到達目標到達レベル授業週
専門的能力分野別の専門工学情報系分野プログラミング与えられたソースプログラムを解析し、プログラムの動作を予測することができる。4
ソフトウェアソースプログラムを解析することにより、計算量等のさまざまな観点から評価できる。4
同じ問題を解決する複数のプログラムを計算量等の観点から比較できる。4
情報数学・情報理論離散数学に関する知識をアルゴリズムの設計、解析に利用することができる。4

評価割合

試験発表相互評価態度ポートフォリオレポート合計
総合評価割合50000050100
基礎的能力2000002040
専門的能力3000003060
分野横断的能力0000000