CMD体育_cmd体育平台@

シラバス参照

授業情報／Course information

科目名／Course: システム検証論／System Verification and Validation
科目一覧へ戻る	2024/09/10 現在

授業基本情報
授業概要情報
授業計画詳細情報
授業評価詳細情報

授業基本情報

科目名（和文）／Course	システム検証論
科目名（英文）／Course	System Verification and Validation
時間割コード／Registration Code	66001601
学部（研究科）／Faculty	情報系工学研究科博士前期課程
学科（専攻）／Department	システム工学専攻
担当教員（○：代表教員）／Principle Instructor （○） and Instructors	○横川　智教
オフィスアワー／Office Hour	横川　智教(前期：火曜2限，後期：火曜2限（出張等で不在にする場合があります）)
開講年度／Year of the Course	2024年度
開講期間／Term	後期
対象学生／Eligible Students	1年,2年
単位数／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	[モデル検査とは] モデル検査とは，モデル化のプロセス，状態爆発への対処について概説する．
2	2?3	[ハードウェア?ソフトウェアのモデル化] クリプキ構造によるソフトウェアやハードウェアのモデル化について解説する．
3	4?5	[時相論理] 計算木論理 CTL* の文法と意味論，CTL* ベースのその他の時相論理について解説する．
4	6?8	[モデル検査アルゴリズム] CTL モデル検査アルゴリズムについて解説する．
5	9?10	[記号モデル検査] 順序付二分決定グラフ (OBDD)と OBDD 表現に基づく記号モデル検査について解説する．
6	11?12	[SAT に基づく有界モデル検査] 命題論理の充足可能性判定（SAT）と SAT に基づく有界モデル検査について解説する．
7	13	[抽象化] モデル検査のコスト削減技術の一つである抽象化について解説する．
8	14?15	[モデル検査ツールとその使い方] モデル検査ツール NuSMV のインストールと利用方法について解説する．

授業評価詳細情報

到達目標及び観点／Learning Goal and Specific Behavioral Viewpoints

No.	到達目標／Learning Goal	知識?理解／Knowledge & Undestanding	技能?表現／Skills & Expressions	思考?判断／Thoughts & Decisions	伝達?コミュニケーション／Communication	協働／Cooperative Attitude
1	システム検証の要素技術について幅広く理解し，実際の問題に対して適用できる（A-1）．	○	○

成績評価方法と基準／Evaluation of Achievement

※出席は2/3以上で評価対象となります。

No.	到達目標／Learning Goal	定期試験／Exam.	レポート
1	システム検証の要素技術について幅広く理解し，実際の問題に対して適用できる（A-1）．		○

評価割合（％）／Allocation of Marks			100

科目一覧へ戻る