シラバス参照

授業情報／Course information

科目名／Course: 計算機援用検証論（R4以前入学生用）／Computer-Aided Verification
科目一覧へ戻る 2024/09/10 現在

授業基本情報
科目名（和文）
／Course		 計算機援用検証論（R4以前入学生用）
科目名（英文）
／Course		 Computer-Aided Verification
時間割コード
／Registration Code		 81A17702
学部（研究科）
／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 [事例紹介]
コンピュータを用いた検証自動化の適用事例について紹介する．
授業評価詳細情報
到達目標及び観点／Learning Goal and Specific Behavioral Viewpoints
No. 到達目標
／Learning Goal		 知識?理解
／Knowledge & Undestanding		 技能?表現
／Skills & Expressions		 思考?判断
／Thoughts & Decisions		 伝達?コミュニケーション
／Communication		 協働
／Cooperative Attitude
1 検証自動化のための要素技術について幅広く理解し，実際の問題に対して適用できる（A）． ○ ○
成績評価方法と基準／Evaluation of Achievement
※出席は2/3以上で評価対象となります。
No. 到達目標
／Learning Goal		 定期試験
／Exam.		 レポート
1 検証自動化のための要素技術について幅広く理解し，実際の問題に対して適用できる（A）． ○
評価割合（％）
／Allocation of Marks		 100

科目一覧へ戻る