FDR（ソフトウェア）

FDR ( Failures-Divergences Refinement ) およびそれに続くFDR2、FDR3、FDR4 は、通信シーケンシャルプロセス(CSP)で表現された形式モデルをチェックするように設計された、リファインメントチェックソフトウェアツールです。これらのツールは元々 Formal Systems (Europe) Ltd. によって開発されました^{[ 1 ]。}オックスフォード大学コンピュータサイエンス学部のBill Roscoeがツールで使用されるアルゴリズムの多くを考案し、Michael Goldsmith ^{[ 2 ]}が実装に大きく貢献しました^{[ 3 ]} 。FDR2 はオックスフォード大学コンピュータサイエンス学部 によって開発され、学術用途やその他の非商用用途で無料で利用できました^{[ 4 ] 。}

FDR はモデル チェッカーとして説明されることが多いが、厳密には改良チェッカーである。これは、2 つの CSP プロセス式をラベル付き遷移システム(LTS) に変換し、特定の意味モデル(トレース、障害、障害/分岐、その他の代替案)内で、一方のプロセスが他方のプロセスの改良であるかどうかを判断するためである。 ^{[ 5 ]} FDR2 は、改良チェック中に探索する必要のある状態空間のサイズを削減するために、さまざまな状態空間圧縮アルゴリズムをプロセス LTS に適用する。

FDR2 は、1995 年に以前のツールである FDR1 に取って代わって以来、多くのリリースを経てきました。FDR3 は、並列実行や統合型チェッカーなどを組み込んだ完全に書き直されたバージョンです。FDR3 は、2008 年から 2012 年の間に FDR2 もリリースしたオックスフォード大学によってリリースされています。 ^{[ 6 ]} FDR3 には ProBE CSP アニメーターが統合されています。現在は FDR4 に置き換えられています。FDR4 は Cocotec から入手できます。^{[ 7 ]}