授業の目的 【日本語】
Goals of the Course(JPN) | | 高度で複雑な情報システムの動作の正しさを検証するため，数理論理学的モデルにもとづく検証支援ツールが実用化されている。本講義では，以下の2つのシステム検証手法を検証ツールの利用を通じて習得する。
(1)モデル検査：モデル検査ツールSpinを用いて，システムの動作において指定される性質を満たさない動作例（反例）がないかどうかを検査することで効率的に不具合を発見する手法について学ぶ。
(2)定理証明：証明支援ツールCoqを用いて，計算機上での証明の記述・検証を体験する。この枠組のもとで，プログラムの正しさを数学的な厳密さで保証する手法について学ぶ。 |
|
|
授業の目的 【英語】
Goals of the Course | | Practical verification tools have been developed based on mathematical models to verify the correctness of complex information systems. This lecture explains the verification techniques of model-checking and theorem-proving for information systems by using existing verification tools.
(1) Model Checking: Using SPIN model checking tool, we learn how to efficiently find a faulty behavior from a program specification by searching counterexamples.
(2) Therem Proving: Using Coq theorem prover, we exercies how to describe proofs with compters. We learn how to show correctness of program. |
|
|
到達目標 【日本語】
Objectives of the Course(JPN) | | | 高度で複雑な情報システムの動作の正しさを検証するため，数理論理学的モデルにもとづく検証支援ツールが実用化されている。本講義では，モデル検査と定理証明の2つのシステム検証手法を，実際に検証ツールを利用することを通じて習得し、利用によって情報システムの検証ができることを目的とする。 |
|
|
到達目標 【英語】
Objectives of the Course | | | We exercise to verify correctness of information systems and learn how to mechanize the verification in practice although it is an undecidable problem in general. This lecture gives the foundations for two well-known method: model-checking and theorem proving and provides the basic ideas for practical verification of information systems. |
|
|
授業の内容や構成
Course Content / Plan | | モデル検査と定理証明について解説し，それぞれ以下のとおり実際の検証ツールを用いた演習を行なう。
モデル検査：モデル検査ツールSpinなどを用いて，システムの動作において指定される性質を満たさない動作例（反例）がないかどうかを検査することで効率的に不具合を発見する手法について学ぶ。
定理証明：証明支援ツールCoqを用いて，計算機上での証明の記述・検証を体験する。この枠組のもとで，プログラムの正しさを数学的な厳密さで保証する手法について学ぶ。
1. 導入
2. モデル検査の概要
3. モデル検査ツールを用いた演習
4. 定理証明系による検証
5. 定理証明系を用いた演習
6. 総括 | Providing basic explanations of model-checking and therem proving, we exercise the verifcation tools of SPIN and Coq.
(1) Model-checking: Using SPIN model-checking tools, we learn how to specify the behavioral properties by temporal logic. The technique to derive counterexamples against the properties mechanically using SPIN.
(2) Therem-proving: Using Coq theorem prover, we exercise to describe proofs for software verification and prove theorems by Coq. We learn how to prove correctness of programs rigorously with a mathematical method.
1. Introduction
2. Overview of Model-checking
3. Exercises of SPIN Model-checking tool
4. Verfication by theorem proving
5. Exercises of Coq Theorem-prover
6. Summary |
|
|
履修条件・関連する科目
Course Prerequisites and Related Courses | | | 論理学2c, オートマトン・形式言語および演習 | | Logic 2c, Automata and Formal Languages |
|
|
成績評価の方法と基準
Course Evaluation Method and Criteria | | 演習課題の評価60％，レポート40％，合計100点満点で60点以上を合格とする。
情報システムをツールを用いて記述して数理モデルに基づく検証できることを評価の基準とする。 | 60% by the exercises given at each lecture and 40% by the term-end report assignment.
A student needs to be able to descript the requirements for an information systems and test and verify the system efficently through the usage of existing major model-chekcing tools and theorem-provers. |
|
|
教科書・参考書
Textbook/Reference book | | | 必要に応じて資料を配布する。 | | The necessary materials are given in the lecture |
|
|
課外学習等（授業時間外学習の指示）
Study Load(Self-directed Learning Outside Course Hours) | | | 演習課題を出す。 | | We give exercises to improve understandings. |
|
|
授業開講形態等
Lecture format, etc. | | |
|
遠隔授業（オンデマンド型）で行う場合の追加措置
Additional measures for remote class (on-demand class) | | |
|