FDR (software) とは

FDR(Failures-Divergences Refinement)とその後のFDR2は、CSP(Communicating sequential processes)で表現された正式なモデルをチェックするように設計された洗練チェックソフトウェアツールです。このツールはもともとFormal Systems(Europe)Ltd.が開発したもので、オックスフォード大学コンピュータサイエンス学科のBill Roscoe氏は、このツールで使用されているアルゴリズムの多くを考案し、Michael Goldsmith氏は実装に役立ちました。 FDR2は、オックスフォード大学コンピュータサイエンス学科によって開発されたもので、学術およびその他の非営利目的で自由に利用できます。
FDRは、しばしばモデルチェッカーと呼ばれますが、技術的には2つのCSPプロセス式をラベル付き遷移システム(LTS)に変換し、プロセスの1つが特定のセマンティック内で他のものを洗練するかどうかを決定するという点で、モデル(トレース、失敗、失敗/発散、その他の選択肢)。 FDR2は、詳細化検査中に探索されなければならない状態空間のサイズを縮小するために、様々な状態空間圧縮アルゴリズムをプロセスLTSに適用する。
FDR2は1995年にFDR1と呼ばれていた以前のツールを置き換え、多くのリリースを経ています.FDR3は、並列実行と統合型チェッカーを組み込んだ完全に書き直されたバージョンです。 FDR3はオックスフォード大学からもリリースされ、2008-12年にFDR2もリリースされました。 ProBE CSP AnimatorはFDR3に統合されています。今はFDR4に引き継がれています。