基礎理論
平成24年度シラバス
２０１２年１月１３日
国立情報学研究所
トップエスイープロジェクト
代表者 本位田 真一
基礎理論講座
磯部 祥尚、粂野 文洋、櫻庭 健年、田辺 良則、石川 冬樹
トップエスイープログラムにおいては様々な分野の最新技術、開発方法論、ツールの利用方法について学ぶ。しかし、トップエスイーの養成対象である、情報系学科を卒業している対象者といえども、必ずしも全ての予備知識を大学、大学院で学んでいる訳ではない。
そこで本教育プログラムにおける様々な講座を受講するための予備知識を補完するために本講座は作成された。
各講座を履修するにあたり、様々な前提知識が求められる。形式仕様講座コースにおいては集合論、論理学の知識が最低限必要であり、モデル検査講座コースにおいては、時相論理、時相論理のモデル検査方法、時相論理式によるシステムの性質の記述から、効率的な実装方法、（時間）オートマトン理論など、広範囲に渡った知識が要求される。本講座は、このように各講座を履修するために必要な予備知識を、関連講座に準じて学べるように設計されている。
本講座において習得できる知識と各講座体系との対応表を次に示す。
|
コース |
形式仕様コース |
モデル検証コース |
|
知識 |
集合論 命題論理学 一階述語論理 再帰的データ構造とその上の帰納法 |
並行プログラム 時相論理 オートマトン理論 モデル検査アルゴリズムとその最適化手法 |
5. 前提知識
本講座を履修するにあたり前提知識は必要とされない。
講義の概要を述べる。
第１回：概論
第２、３、４、５回：論理学と集合
第６回：基礎理論のプログラム検証への活用
第７、８回：形式仕様記述・プログラム検証の基礎，ツール
第９、１０回：時相論理
第１１、１２回：オートマトン
第１３、１４回：モデル検査基礎
第１５回：モデル検査ツール
詳細計画：
·
第１回：概論
·
第２回：命題論理学
Ø
命題論理の演算
Ø
公理と推論
·
第３，４回：述語論理
Ø
量化記号
Ø
意味論、公理系
·
第５回：集合
Ø
集合演算、関数
Ø
列、バグ
·
第６回：プログラムの正しさと検証アプローチ
Ø
逐次プログラム
Ø
並行プログラム
·
第７回：プログラム検証
Ø
ホーア論理
Ø
プログラム検証
·
第８回：リファインメント、形式仕様記述の手法・ツール
Ø
refinement calculus
Ø
VDM、B、Event-B、Alloy
Ø
通信
·
第９回：時相論理
Ø
PLTL、 CTL、CTL*
Ø
意味論、公理系
·
第１０回：検証性質の記述
Ø
到達可能性、安全性、活性、公平性
Ø
性質記述のパターン
·
第１１回：オートマトン１
Ø 有限オートマトン
Ø 正規表現
·
第１２回：オートマトン２
Ø Büchiオートマトン
Ø 時間オートマトン
Ø 並行システムのモデル化
·
第１３回：
モデル検査基礎１
Ø
CTLモデル検査
Ø
時間CTLモデル検査
·
第１４回：
モデル検査基礎２
Ø
PLTLモデル検査
·
第１５回：モデル検査ツール
Ø
SPIN, SMV, LTSA,
UPPAAL
本講座を受講することにより、効率的に他講座の学習を進めることが出来るようになる。
特になし。
9.
評価
各週単位で出題される課題のレポート、出席日数を総合して評価する。
10. 教科書/参考書
· 磯部、櫻庭、田口、田原、粂野: “ソフトウェア科学基礎” (近代科学社) 2008
本講座における教科書。
· 林 晋: "プログラム検証論" (共立出版) 1995（入手困難）
プログラムの正しさに関する理論、ホーア論理を解説したものである。
· Ralph-Johan Back, Joakim Wright: "Refinement Calculus: A Systematic Introduction". Springer, 1998
具体的なモデルが抽象的なモデルに「正しく準拠」しているか、といったプログラムの正しさとリファインメントに関する理論を解説したものである。
· B. Berard et. al.: “Systems and Software Verification: Model-Checking Techniques and Tools”. Springer, 2001.
モデル検査手法を利用したソフトウェア検証について、入門から実践までの一通りが述べられている。
· E. M. Clarke et. al,: “Model Checking”. MIT Press, 2000.
モデル検査手法の原理を理論的に述べたものである。