  シラバス参照
|
| 科目名／Course: 計算機援用検証論／Computer-Aided Verification | |
| 科目一覧へ戻る | 2024/03/25 現在 |
| 科目名（和文） ／Course |
計算機援用検証論 |
|---|---|
| 科目名（英文） ／Course |
Computer-Aided Verification |
| 時間割コード ／Registration Code |
81A17701 |
| 学部（研究科） ／Faculty |
情報系工学研究科 博士後期課程 |
| 学科（専攻） ／Department |
システム工学専攻 |
| 担当教員（○：代表教員）
／Principle Instructor （○） and Instructors |
○横川 智教 |
| オフィスアワー ／Office Hour |
横川 智教(前期：火曜2限，後期：火曜2限 （出張等で不在にする場合があります）) |
| 開講年度 ／Year of the Course |
2024年度 |
| 開講期間 ／Term |
前期 |
| 対象学生 ／Eligible Students |
1年,2年,3年 |
| 単位数 ／Credits |
2 |
| 更新日 ／Date of renewal |
2024/02/29 |
|---|---|
| 使用言語 ／Language of Instruction |
日本語 |
| オムニバス ／Omnibus |
該当なし |
| 授業概略と目的 ／Cource Description and Objectives |
ソフトウェア?ハードウェアシステムは大規模化?複雑化が進んでおり，開発コストの削減ならびにプロダクトの高品質化?高信頼化の実現のためには，システムの検証を適切に実施することが必要不可欠である． 本講義では，計算機を用いてシステムの検証を自動化するための方法論について概説する． |
| 履修に必要な知識?能力?キーワード ／Prerequisites and Keywords |
離散数学およびソフトウェア工学に関する基礎知識が不十分である場合，講義のみで内容を理解することは困難と考えられる． キーワード：形式仕様記述，形式検証，モデル検査，ソフトウェアテスト |
| 履修上の注意 ／Notes |
特になし． |
| 教科書 ／Textbook(s) |
特になし． |
| 参考文献等 ／References |
[1] Edmund M. Clarke, Jr., Orna Grumberg, Daniel Kroening, Doron Peled and Helmut Veith. Model Checking Second Edition. MIT press, 2018. [2] Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith and Roderick Bloem. Handbook of Model Checking, Springer, Cham, 2018. |
| 自主学習ガイド ／Expected Study Guide outside Coursework/Self-Directed Learning Other Than Coursework |
授業中に提示する参考文献を自習することで，より理解度が深まると思われる． |
| 資格等に関する事項 ／Attention Relating to Professional License |
特になし． |
| アクティブラーニングに関する事項 ／Attention Relating to Active Learning |
本科目では以下のアクティブラーニングを採用している． ?プレゼンテーション ?課題（宿題等） |
| 実務経験に関する事項 ／Attention Relating to Operational Experiences |
該当しない． |
| 備考 ／Notes |
本科目は，一部または全部をオンライン授業で実施する可能性がある． |
| No. | 単元（授業回数） ／Unit (Lesson Number) |
単元タイトルと概要 ／Unit Title and Unit Description |
時間外学習 ／Preparation and Review |
配付資料 ／Handouts |
|---|---|---|---|---|
| 1 | 1?5 | [ソフトウェア?ハードウェアの検証技術について] ソフトウェア?ハードウェアの検証技術について概説する． |
||
| 2 | 6?10 | [検証の自動化技術について] コンピュータを用いて検証を自動化するための技術について概説する． |
||
| 3 | 11?15 | [事例紹介] コンピュータを用いた検証自動化の適用事例について紹介する． |
| No. |
到達目標 ／Learning Goal |
知識?理解 ／Knowledge & Undestanding |
技能?表現 ／Skills & Expressions |
思考?判断 ／Thoughts & Decisions |
伝達?コミュニケーション ／Communication |
協働 ／Cooperative Attitude |
||
|---|---|---|---|---|---|---|---|---|
| 1 | 検証自動化のための要素技術について幅広く理解し，実際の問題に対して適用できる（A）． | ○ | ○ |
| No. |
到達目標 ／Learning Goal |
定期試験 ／Exam. |
レポート | ||||
|---|---|---|---|---|---|---|---|
| 1 | 検証自動化のための要素技術について幅広く理解し，実際の問題に対して適用できる（A）． | ○ | |||||
|
評価割合（％） ／Allocation of Marks |
100 | ||||||