シラバス参照

授業情報／Course information

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

授業基本情報
科目名（和文）
／Course		 システム検証論
科目名（英文）
／Course		 System Verification and Validation
時間割コード
／Registration Code		 66001601
学部（研究科）
／Faculty		 情報系工学研究科 博士前期課程
学科（専攻）
／Department		 システム工学専攻
担当教員（○：代表教員）
／Principle Instructor （○） and Instructors		 ○横川　智教
オフィスアワー
／Office Hour		 横川　智教(前期：火曜4限，後期：火曜3限
（出張等で不在にする場合があります）)
開講年度
／Year of the Course		 2023年度
開講期間
／Term		 後期
対象学生
／Eligible Students		 1年,2年
単位数
／Credits		 2
授業概要情報
更新日
／Date of renewal		 2023/03/06
使用言語
／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

科目一覧へ戻る