学部・大学院区分情報学部
時間割コード1001339
科目区分
専門科目(コンピュータ科)関連専門科目(自然，人社)
科目名　【日本語】システム検証及び演習
科目名　【英語】System Verification
コースナンバリングコード
担当教員　【日本語】結縁　祥治 ○ 中澤　巧爾
担当教員　【英語】YUEN Shoji ○ NAKAZAWA Koji
単位数1
開講期・開講時間帯春１期 木曜日 ２時限
Spring1 Thu 2
対象学年４年
4
授業形態講義及び演習
開講系（学部）・開講専攻（大学院）
CS共通
必修・選択
選択


授業の目的　【日本語】
高度で複雑な情報システムの動作の正しさを検証するため，数理論理学的モデルにもとづく検証支援ツールが実用化されている。本講義では，以下の2つのシステム検証手法を検証ツールの利用を通じて習得する。
・モデル検査：Spin/NuSMVなどを用いて，システムの動作において指定される性質を満たさない動作例（反例）がないかどうかを検査することで効率的に不具合を発見する手法について学ぶ。
・定理証明：証明支援ツールCoqを用いて，計算機上での証明の記述・検証を体験する。この枠組のもとで，プログラムの正しさを数学的な厳密さで保証する手法について学ぶ。
授業の目的　【英語】
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.
到達目標　【日本語】
高度で複雑な情報システムの動作の正しさを検証するため，数理論理学的モデルにもとづく検証支援ツールが実用化されている。本講義では，モデル検査と定理証明の2つのシステム検証手法を，実際に検証ツールを利用することを通じて習得する。
到達目標　【英語】
授業の内容や構成
モデル検査と定理証明について解説し，それぞれ以下のとおり実際の検証ツールを用いた演習を行なう。
モデル検査：Spin/NuSMVなどを用いて，システムの動作において指定される性質を満たさない動作例（反例）がないかどうかを検査することで効率的に不具合を発見する手法について学ぶ。
定理証明：証明支援ツールCoqを用いて，計算機上での証明の記述・検証を体験する。この枠組のもとで，プログラムの正しさを数学的な厳密さで保証する手法について学ぶ。

1. 導入
2. モデル検査の概要
3. モデル検査ツールを用いた演習
4. 定理証明系による検証
5. 定理証明系を用いた演習
6. 総括
履修条件・関連する科目
成績評価の方法と基準
演習課題の評価60％，レポート40％，合計100点満点で60点以上を合格とする。
教科書・参考書
必要に応じて資料を配布する。
課外学習等（授業時間外学習の指示）
演習課題を出す。
授業開講形態等
遠隔授業（オンデマンド型）で行う場合の追加措置