| 日時： | 2009年12月14日 10:00〜17:00 |
| 場所： | 国立情報学研究所（東 京都千代田区） |
| 題目： | 並行システムの検証と実装 （入門編） |
| 概要： | 本セミナーでは、並行システムの信頼性を高めることを目的として、並行 システムをプロセス代数CSP (Communicating Sequential Processes) でモデル化し、モデル検査器FDRで検証し、JavaライブラリJCSPで実装する方法について説明します。CSPは並行システムを解析するための理論、 FDRはCSPモデルを検証するためのツール、JCSPはCSPモデルを並列/分散実行するためのライブラリです。本セミナーの特徴は、CSP理論 →FDR検証→JCSP実装の流れを重視していることにあります。FDRとJCSPの使い方を習得することによって、並行システムのCSPによるモデル化 と検証の考え方をより深く理解することができます。 |
| プロセス
代数CSP |
| プロセス代数は並行システムを解析するための理論であり、CSPは代表 的なプロセス代数の一つです。CSPによる並行動作記述（CSPの構文）、遷移規則や失敗等価/詳細化（CSPの意味）について説明します。 |
| モデル検 査器FDR |
| FDRはCSPモデルの詳細化関係を検査するためのツールです。検証に
おける詳細化関係の使い分けや、デバッガの使い方について説明します。 |
| Java ライブラリJCSP |
| JCSPはCSPモデルを並列/分散実行するためのライブラリです。 CSPモデルをJCSPプログラムに変換するポイントについて説明します。 |