講義概要
ロボットなどの制御ロジックの複雑な振舞いを表現する方法のひとつとして有限状態機械が広く使われている。本講義では、協調する有限状態機械の設計の信頼性向上を目的とし、有限状態機械の形式的な記述方法と網羅的な検証方法の習得を目標とする。本講義の前半で、形式仕様記述言語CSPとモデル検査器FDRについて解説し、後半で、協調する有限状態機械のCSPによる形式的な記述と、FDRによる網羅的な検証の演習を行う。講師
- 所属
- 産業技術総合研究所
- 講師名
- 磯部 祥尚
１９９２年 芝浦工業大学大学院電気工学専攻修士課程修了。同年、通商産業省工業技術院電子技術総合研究所 入所。２００１年 独立行政法人産業技術総合研究所に改組し、現在 国立研究開発法人産業技術総合研究所 情報技術研究部門 ソフトウェアアナリティクス研究グループ 主任研究員 工学博士。主に並行プロセスの形式記述と検証に関する研究・教育、並行処理解析ツールの開発に従事。
講義内容
先ず、協調する有限状態機械によって制御される分散システムの例（協調搬送ロボットを予定）をもとに、協調する有限状態機械の設計の難しさを説明し、その設計を支援するために、形式的な記述と網羅的な検証が有効であることを説明する。次に、協調する簡単な有限状態機械の例をもとに、形式仕様記述言語CSPによる有限状態機械の形式的な記述方法と、モデル検査器FDRによる協調動作の網羅的な検証方法を解説する。その後、CSPとFDRを用いて、協調する有限状態機械の記述と検証の演習を行う。
講義内容
- 背景：協調する有限状態機械の設計の難しさの説明
- 記述：CSPによる有限状態機械の形式記述の解説
- 検証：FDRによる協調動作の検証方法の解説
演習内容
- 記述：CSPによる有限状態機械の形式記述の作成
- 検証：FDRによる協調動作の検証の実習
受講要件
- 【受講要件】
- 特になし
- 【事前学習のポイント】
- 特になし
教科書
講義２週間前に電子ファイル送付（事前学習を推奨）講義に関連する解説記事・参考文献・図書等
- [1] 磯部祥尚（著）, 並行システムの検証と実装 ― 形式手法CSPに基づく高信頼並行システム開発入門, 近代科学社, 2012. https://sites.google.com/site/topsevic/home
- [2] 磯部祥尚, モデル検査による設計検証, 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