学部・大学院区分
Undergraduate / Graduate
情報・博前
時間割コード
Registration Code
2550050
科目区分
Course Category
主専攻科目
科目名 【日本語】
Course Title
ソフトウェア基礎論特論B
科目名 【英語】
Course Title
Advanced Lectures on Foundations of Software B
コースナンバリングコード
Course Numbering Code
GSI156042J
担当教員 【日本語】
Instructor
結縁 祥治 ○
担当教員 【英語】
Instructor
YUEN Shoji ○
単位数
Credits
1
開講期・開講時間帯
Term / Day / Period
秋2期 月曜日 3時限
Fall2 Mon 3
対象学年
Year
1年
1
授業形態
Course style

開講系(学部)・開講専攻(大学院)
Subject
情報システム学専攻
必修・選択
Required / Selected


授業の目的 【日本語】
Goals of the Course(JPN)
本講義では、モデル検査の基礎とその応用について習得する。モデル検査は
情報システムが正しく動作することを確認するために一般的に用いられる手法と
なっている。 モデル検査を用いることで特に並行システムのような複雑なシステムの
不具合を効果的に見つけ出すことができる。モデル検査の基礎的概念と適用のための
具体的な最適化技法、抽象化技法について議論する。
授業の目的 【英語】
Goals of the Course
This course presents the basics and applications of model-checking techniques.
Recently model-checking has become a standard technique to
ensure information systems behave correctly. The technique is
often very effective in mechanically finding unexpected ill behavior of
concurrent systems, which is often difficult to be detected by hand.
This course shows the basic concept of model-checking and
effective optimization techniques.
到達目標 【日本語】
Objectives of the Course(JPN)
コンピュータシステムの振舞いの正しさを検証する形式手法としてモデル検査の手法について説明する。
到達目標 【英語】
Objectives of the Course
Learning 'Model-Checking' fundamentals as a formal-method technique
for supporting the reliability of software systems
授業の内容や構成
Course Content / Plan
情報システムの複雑化に伴い,システムが正しくに動作するかどうかを経験的に検証することは困難になっている。
形式手法のひとつであるモデル検査は,数理的に構築した振舞いモデルに情報システムが合致するかどうかを検査し,合致しない振舞いを効率的に探し出す手法である。
検査技法の発達により,実用的なシステムに対してもモデル検査を適用し,通常では発見困難なエラーを発見することに成功している例が知られている。
本講義では,モデル検査の基本的な概念と効率的な検査技法について習得する。

〔計画〕
1. モデル検査概要
2. 線形時間的性質と線形時相論理
3. 安全性解析
4. 活性解析
5. 公平性条件
6. ω言語と線形時相論理
7. モデル検査アルゴリズムと検査ツール
8. 総括
This lecture gives the fundamentals for the model-checking technique.
'Model-checking' is one of the well-known formal methods to improve the reliability of software systems based on the mathematical
and logical foundation, checking if the behavior of a system accords with the
required properties. The checking procedures have been actively studied
to efficiently check a practical software system with reasonable
accuracy by finding counterexamples.

1. Introduction
2. Linear-time properties and linear temporal logic(LTL)
3. Safety analysis
4. Liveness analysis
5. Fairness
6. Omega-language and LTL
7. Model-checking procedures
8. Conclusion
履修条件・関連する科目
Course Prerequisites and Related Courses
ソフトウェア基礎論特論A
成績評価の方法と基準
Course Evaluation Method and Criteria
提出されたレポートの内容を評価する。100点中60点で合格とする。
時相論理による振舞い性質の記述とモデル検査技法についての習得によって評価する。
Assignments are evaluated. 60 out of 100 are required to pass.
A student needs to acquire the basic knowledge of temporal logic for describing properties and be able to explain the primary mechanism for model-checking for the qualification.
教科書・参考書
Textbook/Reference book
E.M. Clarke Jr, O. Grumberg, D. Kroening, D. Peled, and H. Veith: Model Checking , Second Edition
MIT Press, 2018, ISBN 9780262038836
E.M. Clarke Jr, O. Grumberg, D. Kroening, D. Peled, and H. Veith: Model Checking , Second Edition
MIT Press, 2018, ISBN 9780262038836
課外学習等(授業時間外学習の指示)
Study Load(Self-directed Learning Outside Course Hours)
講義の内容に基づいてレポートの提出を求める
Submissions of assignments are required.
授業開講形態等
Lecture format, etc.
対面を原則とするが,必要に応じてリモート配信を行う場合がある.
遠隔授業(オンデマンド型)で行う場合の追加措置
Additional measures for remote class (on-demand class)