シラバス参照
|
シラバス参照
|
| 講義概要/Course Information |
| 科目基礎情報/General Information |
| 授業科目名 /Course title (Japanese) |
ソフトウェア基礎特論 | ||
|---|---|---|---|
| 英文授業科目名 /Course title (English) |
Advanced Theory of Software Sciences | ||
| 科目番号 /Code |
|||
| 開講年度 /Academic year |
2019年度 | 開講年次 /Year offered |
全学年 |
| 開講学期 /Semester(s) offered |
前学期 | 開講コース・課程 /Faculty offering the course |
博士前期課程、博士後期課程 |
| 授業の方法 /Teaching method |
講義 | 単位数 /Credits |
2 |
| 科目区分 /Category |
大学院専門教育科目 - 専門科目Ⅱ | ||
| 開講類・専攻 /Cluster/Department |
情報・ネットワーク工学専攻 | ||
| 担当教員名 /Lecturer(s) |
○中野 圭介 | ||
| 居室 /Office |
|||
| 公開E-mail |
nakano ＠ uec.ac.jp | ||
| 授業関連Webページ /Course website |
講義内にてお知らせします． | ||
| 更新日 /Last update |
2019/03/04 19:05:17 | 更新状況 /Update status |
公開中 /now open to public |
| 講義情報/Course Description |
| 主題および 達成目標（2,000文字以内） /Themes and goals（up to 2,000 letters） |
ソフトウェアを検証する形式手法を学習する．コンピュータの計算能力の向上 に伴い，昨今では，電子機器や家電だけでなく，自動車や航空機・ロケットな どの大規模なものまでがソフトウェアにより制御されることが標準となりつつ ある．このようなソフトウェアに意図しないバグが存在する場合，人命に関わ る事故や企業の存亡に影響する損害に繋がる可能性すら考えられる．実際，制 御ソフトウェアの欠陥によるロケット打ち上げの失敗や，プログラムのチェッ ク漏れのために大損害を被った銀行などの事例が絶えずニュースとなっている． このため，「ソフトウェアが意図通りに正しく動作すること」を保証すること は非常に重要である．本講義では，これを解決する形式的検証手法の基礎を学 び，広く用いられているモデル検査システムの使い方を学習する． |
|---|---|
| 前もって履修 しておくべき科目（1,000文字以内） /Prerequisites（up to 1,000 letters） |
なし |
| 前もって履修しておくこ とが望ましい科目（1,000文字以内） /Recommended prerequisites and preparation（up to 1,000 letters） |
離散数学, 論理回路学, オートマトン理論 |
| 教科書等（1,000文字以内） /Course textbooks and materials（up to 1,000 letters） |
受講の助けになる書籍を以下に挙げるので参考にされたい． - Systems and Software Verification ─ Model-Checking Techniques and Tools By B. Bérard et al. Springer |
| 授業内容と その進め方（2,000文字以内） /Course outline and weekly schedule（up to 2,000 letters） |
大まかな講義内容は以下の通りで，集中講義の形式で実施する． 1. ソフトウェアの検証とは 2. 状態遷移系 3. 並行処理モデル 4. ブッキオートマトン 5. 安全性・活性・公平性 6. モデル検査 7. 線形時相論理 (LTL) 8. LTL における公平性とモデル検査 9. SPIN を利用したモデル検査 10. 計算木論理 (CTL) 11. CTL における公平性とモデル検査 12. SMV を利用したモデル検査 13. 定理証明支援系 14. より進んだソフトウェア検証 15. まとめと理解度調査 各講義は主にスライド及び板書を通じて行う． |
| 実務経験を活かした 授業内容 (実務経験内容も含む) /Course content utilizing practical experience |
|
| 授業時間外の学習 （予習・復習等）（1,000文字以内） /Preparation and review outside class（up to 1,000 letters） |
|
| 成績評価方法 および評価基準 （最低達成基準を含む） （1,000文字以内） /Evaluation and grading （up to 1,000 letters） |
講義内の理解度調査と課題の提出を通じて評価を行う． |
| オフィスアワー： 授業相談（1,000文字以内） /Office hours（up to 1,000 letters） |
事前にメール等でアポイントをとること． |
| 学生へのメッセージ（1,000文字以内） /Message for students（up to 1,000 letters） |
理解を深めるため講義後の復習を強く推奨する． |
| その他 /Others |
なし |
| キーワード /Keywords |
ソフトウェア検証, 形式手法, モデル検査, 定理証明支援系 |