並行性と状態遷移設計D03-02
講義概要
講座日程：2016年8月9日(半日間）
並行プロセスは、同時に走る複数のプロセスと連携・協調するプロセスであり、マルチコアCPUやネットワークの普及とともに、そのニーズが高まっている。しかし、複数のプロセスの干渉によって発生する並行プロセス特有の不具合は再現性がなく、テストによる発見は困難である。本講座では、並行プロセスを論理的に記述し、網羅的に検証することによって、設計段階で並行プロセスの不具合を発見する方法について説明する。
講師 産業技術総合研究所 磯部 祥尚
1992年 芝浦工業大学大学院電気工学専攻修士課程修了。同年、通商産業省工業技術院電子技術総合研究所 入所。2001年 独立行政法人産業技術総合研究所に改組し、現在（独）産業技術総合研究所 セキュアシステム研究部門 高信頼ソフトウェア研究グループ 研究グループ長。並行プロセスの形式記述と検証に関する研究・教育、並行プロセス解析ツールの開発に従事。
講義内容
並行プロセスの理解力向上を目的として、並行プロセスの論理的な記述方法と網羅的な検証方法の習得を目標とする。そのために、並行プロセスの論理的な記述言語としてCSP、その網羅的な検証ツールとしてFDRを紹介する。
講義内容
- 概要：並行プロセスの概要
- 表現：並行プロセスの状態遷移表現
- 記述：並行プロセスの記述言語CSP
- 検証：並行プロセスの検証ツールFDR
- 用例：並行プロセスのCSP記述例とFDR検証例
演習内容
- 記述：CSPによる並行プロセスの記述
- 検証：FDRによる並行プロセスの検証
受講要件
特になし
教科書
講義２週間前に電子ファイル送付（事前学習を推奨）
講義に関連する解説記事・参考文献等
- 磯部祥尚（著）, 東野輝夫（監修）, 並行システムの検証と実装 ― 形式手法CSPに基づく高信頼並行システム開発入門, 近代科学社, 2012. https://sites.google.com/site/topsevic/home
- 磯部祥尚, モデル検査による設計検証, 6章 CSPによる並行性の設計とFDRを使った検証, コンピュータソフトウェア, Vol.31, No.4, pp.54-58, 2012. https://www.jstage.jst.go.jp/article/jssst/31/4/31_4_40/_pdf
- トップエスイー講座「並行システムの検証と実装」ウェブサイト. https://staff.aist.go.jp/y-isobe/topse/vic/
