形式手法とモデル検査A01-05
講義概要
講座日程：2015年08月26日(１日間）
物理的な実体をもたないソフトウェアは、部品の整合性を確認したり起こりうる振る舞いをもれなく把握することが困難な対象である。本講義ではソフトウェアの構造や性質を厳密に取り扱うことができる数理的なアプローチ(形式手法)を紹介する。特に、振る舞いの網羅的な検証を可能にするモデル検査を実例を交えながら解説する。
講師産業技術総合研究所 セキュアシステム研究部門 西原 秀明 氏
2003年より産業技術総合研究所 システム検証研究ラボ，システム検証研究センターにて形式的検証の適用と普及について研究．特にモデル検査の技術者向け教材作成，知識の整理等に従事。その後組込みシステム技術連携研究体，セキュアシステム研究部門にて形式的モデルベーステスト，高信頼システムの安全分析プロジェクトに参加。システム開発における数理的(形式的)なアプローチの適用拡大を目指して活動中。
講義内容
- システム開発と数理的アプローチ
- ・数理的アプローチの利点，解決する課題
- ・関心の高まり，規格・標準での扱い
- 数理的アプローチ概論
- ・一般的な適用イメージ
- ・形式化・抽象化
- モデル検査
- 概要
- モデル検査ツール
- モデル検査の実際
- モデル検査演習 1
- モデル検査演習 2
- まとめ・関連する話題
受講要件
アーキテクチャ設計コースベース科目修了程度の知識があること．組込みシステムの開発において機能仕様或いはそれに相当する仕様や設計を作成した経験があること．
教科書
講義２週間前に電子ファイル送付（事前学習を推奨）
講義に関連する解説記事・参考文献等
「特集：組込みシステム産業を支える産総研の本格研究」産総研 TODAY Vol. 11-12.
(http://www.aist.go.jp/aist_j/aistinfo/aist_today/vol11_12/vol11_12_main.html)
- 組込みシステム技術連携研究体の活動紹介
- 共同研究事例:形式手法を利用した高信頼ソフトウェアのためのテスト設計技術の開発
- 共同研究事例:上流工程大規模テストのための技術開発
「ソフトウェア工学の道具としての形式手法」中島震著，
NII Technical Report NII-2007-007J. (http://www.nii.ac.jp/TechReports/07-007J.pdf)
