|
授業科目名
|
担当教員
|
|||||||||||||||||||||
|
論理と形式手法
|
岩沼 宏治
|
|||||||||||||||||||||
|
時間割番号
|
単位数
|
コース
|
履修年次
|
期別
|
曜日
|
時限
|
||||||||||||||||
| TCS307 | 2 | (未登録) | 3 | 前期 | 火 | III | ||||||||||||||||
| ［概要］ | ||||||||||||||||||||||
| 数理論理や数理科学に基づく，プログラムやハードウエアの仕様記述，開発と検証法に関する理論と技術について学ぶ。これらは極めて高い信頼性を必要とする大規模システム（例えば CPU，分散並列サーバーシステム，ICカードや自動車などへの組み込みシステムなど）を開発する際の基礎をなす技術である．具体的には，情報処理学会J07-CSの「離散構造」及びJ07-SEの「論理と計算理論」ならびに「形式手法」の項目に準拠し、その一部を取り上げる． | ||||||||||||||||||||||
| ［具体的な達成目標］ | ||||||||||||||||||||||
| 1. 形式的手法の基盤となる数理論理やモデル検査法などの数理科学の基礎について学ぶ。 2. Floyd-Hoare論理や有限状態モデルなどに基づくシステムの記述と，正当性の検証に関すして基本的事項について学ぶ． 3. 幾つかの実例を通して，形式的仕様記述の実際を学ぶ 4. NuSMVなどの形式的な仕様記述検証のためのツールの実際について学ぶ． |
||||||||||||||||||||||
| ［必要知識・準備］ | ||||||||||||||||||||||
| 離散数学（集合，順序，関係など），線形代数，アルゴリズムとデータ構造，プログラミング，オートマトンと形式言語，オペレーティングシステム | ||||||||||||||||||||||
| ［評価方法・評価基準］ | ||||||||||||||||||||||
|
||||||||||||||||||||||
| ［教科書］ | ||||||||||||||||||||||
| (未登録) | ||||||||||||||||||||||
| ［参考書］ | ||||||||||||||||||||||
|
||||||||||||||||||||||
| ［講義項目］ | ||||||||||||||||||||||
| 第1回 命題論理の基礎 第2回 SATソルバーの基礎 第3回 最新SATソルバーの実際 第4回 述語論理の基礎：意味と形式推論体系 第5回 計算可能性と計算量の理論 第6回 正当性検証：システムの正当性とは？： 事後条件、帰納表明 第7回 正当性検証：部分的正当性，停止性証明 第8回 構造化プログラム 第9回 Floyd-Hoare論理 第10回 モデル検査と時相命題論理式 第11回 モデル検査とNuSMV 第12回 演習１：はじめてのNuSMV 第13回 演習２：NuSMV を用いた簡単な仕様記述と検証 第14回 演習３：NuSMV を用いた有限モデル検査 第15回 総合評価（総括とまとめ） |
||||||||||||||||||||||
| ［教育方法］ | ||||||||||||||||||||||
| 講義と演習を組み合わせた教育を行い，全ての講義演習の資料をPowerPointを利用して電子的に作成し，ホームページから配布する予定だる． • 適宜，自主勉強用の演習問題プリントを配布する． • 部分的にNuSMV等のツールを用いた演習を行う． |
||||||||||||||||||||||
| ［JABEEプログラムの学習・教育目標との対応］ | ||||||||||||||||||||||
| (未登録) | ||||||||||||||||||||||
| ［その他］ | ||||||||||||||||||||||
| オフィスアワー：月曜４時限目 | ||||||||||||||||||||||