シラバス参照

授業情報／Course information

科目一覧へ戻る 2020/10/22 現在

授業基本情報
科目名（和文）
／Course		 システム検証論
科目名（英文）
／Course		 System Verification and Validation
時間割コード
／Registration Code		 66001601
学部（研究科）
／Faculty		 情報系工学研究科 博士前期課程
学科（専攻）
／Department		 システム工学専攻
担当教員（○：代表教員）
／Principle Instructor （○） and Instructors		 ○横川　智教
オフィスアワー
／Office Hour		 横川　智教(1〜2Q：火曜 4 限，3〜4Q：火曜 3 限，場所：2504
＊授業に関する質問は随時受け付けます．
＊急な会議・出張等のため不在にすることがあります．)
開講年度
／Year of the Course		 2020年度
開講期間
／Term		 後期
対象学生
／Eligible Students		 1年,2年
単位数
／Credits		 2
授業概要情報
更新日
／Date of renewal		 2020/03/10
使用言語
／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.
[3] Glenford J. Myers, Corey Sandler and Tom Badgett. The Art of Software Testing (English Edition) 3rd Edition, Wiley, 2011.
[4] R. Milner, Communication and Concurrency, Prentice Hall, 1995.
自主学習ガイド
／Expected Study Guide outside Coursework/Self-Directed Learning Other Than Coursework		 授業中に提示する参考文献を自習することで，より理解度が深まると思われる．
資格等に関する事項
／Attention Relating to Professional License		 特になし．
備考
／Notes		 特になし．
授業計画詳細情報
No. 単元（授業回数）
／Unit (Lesson Number)		 単元タイトルと概要
／Unit Title and Unit Description		 時間外学習
／Preparation and Review		 配付資料
／Handouts
1 1 [状態機械]
システムの形式的検証の前提となる状態遷移系としてのシステム表現について，オートマトンやクリプキ構造などを例として解説する．
2 2 [リアクティブシステム]
刺激と応答に基づいて動作を行うシステムであるリアクティブシステムについて，ステートチャートなどを用いて解説する．
3 3 [並行システム]
並行システムの代表的なモデルであるペトリネットについて，その記法と意味論について解説する．また，ペトリネットの拡張である時間ペトリネットや確率ペトリネットについても解説する．
4 4 [時相論理]
状態遷移システムの時間的特性を表現する論理である時相論理について解説する．代表的な時相論理である，計算木論理と線形時間論理についても解説する．
5 5 [モデル検査]
システムの自動検証技術であるモデル検査について解説する．また，基本的なモデル検査のアルゴリズムと計算量についても解説する．
6 6 [記号モデル検査]
モデル検査の課題である状態爆発問題について解説し，その解決を目指して開発された記号モデル検査の中でも代表的な技術である，BDD モデル検査とSAT モデル検査について解説する．
7 7 [検査特性]
システムの検査特性である，到達可能性，安全性，活性，非デッドロック性などについて解説する．
8 8 [抽象化]
システムの抽象化技術について，状態合成，変数の抽象化，制約による抽象化などについて解説する．
9 9 [プロセス代数]
システムをプロセスとして表現し，代数的に操作するための手法について解説する．
10 10 [モデル検査ツール]
著名なモデル検査ツールとして，SMV，SPIN，UPPAAL，LTSA，FDRなどについて解説する．
11 11 [ソフトウェアテスト]
ソフトウェアテストの方法論と要素技術について解説する．
12 12 [組合せテスト]
ソフトウェアテストの代表的な手法である組合せテストについて解説する．
13 13 [モデルベーステスト]
モデルベーステストの要素技術について解説する．
14 14 [テストの自動化]
テストの自動化を実現するための技術について解説する．
15 15 [総括]
システム検証の技術動向について解説する．
授業評価詳細情報
到達目標及び観点／Learning Goal and Specific Behavioral Viewpoints
No. 到達目標
／Learning Goal		 知識・理解
／Knowledge & Undestanding		 技能・表現
／Skills & Expressions		 思考・判断
／Thoughts & Decisions		 伝達・コミュニケーション
／Communication		 協働
／Cooperative Attitude
1 システム検証の要素技術について幅広く理解する． ○
成績評価方法と基準／Evaluation of Achievement
※出席は2/3以上で評価対象となります。
No. 到達目標
／Learning Goal		 定期試験
／Exam.		 レポート
1 システム検証の要素技術について幅広く理解する． ○
評価割合（％）
／Allocation of Marks		 100

科目一覧へ戻る