HOME > 人材育成プログラム>講座一覧 > 並行性と状態遷移設計 D03-02

並行性と状態遷移設計D03-02

講義概要

講座日程:2016年8月9日(半日間)

並行プロセスは、同時に走る複数のプロセスと連携・協調するプロセスであり、マルチコアCPUやネットワークの普及とともに、そのニーズが高まっている。しかし、複数のプロセスの干渉によって発生する並行プロセス特有の不具合は再現性がなく、テストによる発見は困難である。本講座では、並行プロセスを論理的に記述し、網羅的に検証することによって、設計段階で並行プロセスの不具合を発見する方法について説明する。

講師  産業技術総合研究所 磯部 祥尚

1992年 芝浦工業大学大学院電気工学専攻修士課程修了。同年、通商産業省工業技術院電子技術総合研究所 入所。2001年 独立行政法人産業技術総合研究所に改組し、現在(独)産業技術総合研究所 セキュアシステム研究部門 高信頼ソフトウェア研究グループ 研究グループ長。並行プロセスの形式記述と検証に関する研究・教育、並行プロセス解析ツールの開発に従事。

講義内容

並行プロセスの理解力向上を目的として、並行プロセスの論理的な記述方法と網羅的な検証方法の習得を目標とする。そのために、並行プロセスの論理的な記述言語としてCSP、その網羅的な検証ツールとしてFDRを紹介する。

講義内容

  • 概要:並行プロセスの概要
  • 表現:並行プロセスの状態遷移表現
  • 記述:並行プロセスの記述言語CSP
  • 検証:並行プロセスの検証ツールFDR
  • 用例:並行プロセスのCSP記述例とFDR検証例

演習内容

  • 記述:CSPによる並行プロセスの記述
  • 検証:FDRによる並行プロセスの検証
並行プロセスの例 FDRによる検証例

受講要件

特になし

教科書

講義2週間前に電子ファイル送付(事前学習を推奨)

講義に関連する解説記事・参考文献等

↑ページトップへ