FDR2とは

FDR2(Failures/Divergence Refinement 2)とはFormal Systems Europe Ltd. が開発したCSPの自動検証ツールである。

CSPで記述したプロセスのRefinment,Deadlock,Livelock,Determinismをチェックすることができる。

上記 Formal Systems のサイトからFDR2、マニュアル等がダウンロードできる。

実行には、環境変数FDRHOMEにFDR2をインストールしたルートディレクトリをセットする必要がある。

FDRHOME=~/FDR2/fdr-2.83-linux-academic
export FDRHOME

実行するとまず、下のようなファイルを選択する画面が出てくる。

CSP記述を含んだファイル（拡張子は.csp）を選択すれば、下記のようなFDR2の実行画面が出てくる。

このツールの使い方についても随時説明していく。