Loading article…
 | |
| その他の名前 | FDR2、FDR3、FDR4 |
|---|---|
| 開発者 | オックスフォード大学、ココテック |
| 安定版リリース | 4.2.4 / 2019年2月19日 |
| オペレーティング·システム |
|
| タイプ | CSPリファインメント チェッカー |
| ライセンス | 独自ソフトウェア |
| Webサイト | https://cocotec.io/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）に変換し、指定されたセマンティックモデル（トレース、障害、障害/発散、その他の選択肢）内でプロセスの1つがもう1つのプロセスのリファインメントであるかどうかを判断します。 [5] FDR2は、リファインメントチェック中に探索する必要がある状態空間のサイズを削減するために、プロセスLTSに さまざまな状態空間圧縮アルゴリズムを適用します。
FDR2は、1995年に現在FDR1と呼ばれている以前のツールに取って代わって以来、多くのリリースが行われてきました。その後、並列実行や統合型チェッカーなどを組み込んだ完全に書き直されたバージョンのFDR3が後継となりました。FDR3はオックスフォード大学によってリリースされましたが、同大学は2008年から2012年にかけてFDR2もリリースしました。[6] ProBE CSP AnimatorはFDR3に統合されています。現在はFDR4が後継となっています。FDR4はCocotecから入手できます。[7]
参考文献
- ^ フォーマルシステムズ（ヨーロッパ）有限会社
- ^ マイケル・ゴールドスミス教授（現在オックスフォード大学教授）。
- ^ Philippa Broadfoot と Bill Roscoe。FDR とその応用に関するチュートリアル。Klaus Havelund、John Penix、Willem Visser (編集者)、SPIN モデル検査とソフトウェア検証、Springer-Verlag、Lecture Notes in Computer Science、第 1885 巻、322 ページ、2000 年。
- ^ ソフトウェア: FDR2、商用ライセンスは Formal Systems (Europe) Ltd. から入手可能。
- ^ AW Roscoe (1994)。「モデル検査 CSP」。A Classical Mind: CAR Hoareを讃えたエッセイ集。Prentice Hall。p. 353。ISBN 9780132948449。
- ^ FDR3の紹介
- ^ ソフトウェア: FDR4、ダウンロードして最初の起動後に商用ライセンスを取得可能