| フランクリン・ルーズベルト | |
|---|---|
 | |
| その他の名前 | FDR2、FDR3、FDR4 |
| 開発者 | オックスフォード大学、ココテック |
| 安定版リリース | 4.2.4 / 2019年2月19日 ( 2019-02-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] FDR3にはProBE CSP Animatorが統合されています。現在は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: Essays in Honour of CAR Hoare . Prentice Hall . p. 353. ISBN 9780132948449。
- ^ FDR3の紹介
- ^ ソフトウェア: FDR4、ダウンロードして最初の起動後に商用ライセンスを取得可能
 | このプログラミングツール関連の記事はスタブです。この記事を充実させることでWikipediaに貢献できます。 |
