FDR (software) (original) (raw)
FDR (Failures-Divergences Refinement) and subsequently FDR2, FDR3 and FDR4 are refinement checking software tools, designed to check formal models expressed in Communicating sequential processes (CSP). The tools were originally developed by Formal Systems (Europe) Ltd. Bill Roscoe of the Department of Computer Science, University of Oxford devised many of the algorithms used by the tool and Michael Goldsmith was instrumental in the implementation. FDR2 was developed by Department of Computer Science, University of Oxford from where it was freely availablefor academic and other non-commercial use.
| Property | Value |
|---|---|
| dbo:abstract | FDR (Failures-Divergences Refinement) and subsequently FDR2, FDR3 and FDR4 are refinement checking software tools, designed to check formal models expressed in Communicating sequential processes (CSP). The tools were originally developed by Formal Systems (Europe) Ltd. Bill Roscoe of the Department of Computer Science, University of Oxford devised many of the algorithms used by the tool and Michael Goldsmith was instrumental in the implementation. FDR2 was developed by Department of Computer Science, University of Oxford from where it was freely availablefor academic and other non-commercial use. FDR is often described as a model checker, but is technically a refinement checker, in that it converts two CSP process expressions into Labelled Transition Systems (LTSs), and then determines whether one of the processes is a refinement of the other within some specified semantic model (traces, failures, failures/divergence and some other alternatives). FDR2 applies various state-space compression algorithms to the process LTSs in order to reduce the size of the state-space that must be explored during a refinement check. FDR2 has gone through many releases, having replaced the earlier tool now referred to as FDR1 in 1995. It has been succeeded by FDR3, a completely re-written version incorporating amongst other things parallel execution and an integrated type checker. FDR3 is released by the University of Oxford, which also released FDR2 in the period 2008-12. A ProBE CSP Animator is integrated in FDR3. It now has been succeeded by FDR4. FDR4 is available from Cocotec. (en) |
| dbo:developer | dbr:University_of_Oxford |
| dbo:genre | dbr:Communicating_sequential_processes |
| dbo:latestReleaseDate | 2019-02-19 (xsd:date) |
| dbo:latestReleaseVersion | 4.2.4 |
| dbo:license | dbr:Proprietary_software |
| dbo:thumbnail | wiki-commons:Special:FilePath/FDR4_CSP_refinement_checker_software_logo.png?width=300 |
| dbo:wikiPageExternalLink | https://cocotec.io/fdr/ |
| dbo:wikiPageID | 25840230 (xsd:integer) |
| dbo:wikiPageLength | 4315 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1081886389 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Bill_Roscoe dbr:Department_of_Computer_Science,_University_of_Oxford dbr:University_of_Oxford dbr:Proprietary_software dbc:Oxford_University_Computing_Laboratory dbr:Communicating_sequential_processes dbr:Michael_Goldsmith_(computer_scientist) dbc:Concurrent_computing dbr:Refinement_(computing) dbc:Model_checkers dbr:Model_checker dbr:Formal_model dbr:Labelled_transition_system dbr:Program_refinement dbr:Software_tool dbr:Semantic_model dbr:State-space |
| dbp:developer | University of Oxford, Cocotec (en) |
| dbp:genre | CSP refinement checker (en) |
| dbp:latestReleaseDate | 2019-02-19 (xsd:date) |
| dbp:latestReleaseVersion | 4.200000 (xsd:double) |
| dbp:license | dbr:Proprietary_software |
| dbp:logo | FDR4_CSP_refinement_checker_software_logo.png (en) |
| dbp:name | FDR FDR2 FDR3 FDR4 (en) |
| dbp:operatingSystem | Linux (en) MacOS (en) Windows (en) (en) |
| dbp:website | https://cocotec.io/fdr/ |
| dbp:wikiPageUsesTemplate | dbt:Infobox_software dbt:Reflist dbt:Start_date_and_age dbt:Use_dmy_dates dbt:Programming-software-stub |
| dct:subject | dbc:Oxford_University_Computing_Laboratory dbc:Concurrent_computing dbc:Model_checkers |
| rdf:type | owl:Thing dbo:Software schema:CreativeWork dbo:Work wikidata:Q386724 wikidata:Q7397 |
| rdfs:comment | FDR (Failures-Divergences Refinement) and subsequently FDR2, FDR3 and FDR4 are refinement checking software tools, designed to check formal models expressed in Communicating sequential processes (CSP). The tools were originally developed by Formal Systems (Europe) Ltd. Bill Roscoe of the Department of Computer Science, University of Oxford devised many of the algorithms used by the tool and Michael Goldsmith was instrumental in the implementation. FDR2 was developed by Department of Computer Science, University of Oxford from where it was freely availablefor academic and other non-commercial use. (en) |
| rdfs:label | FDR (software) (en) |
| owl:sameAs | wikidata:FDR (software) https://global.dbpedia.org/id/4jJWx |
| prov:wasDerivedFrom | wikipedia-en:FDR_(software)?oldid=1081886389&ns=0 |
| foaf:depiction | wiki-commons:Special:FilePath/FDR4_CSP_refinement_checker_software_logo.png |
| foaf:homepage | https://cocotec.io/fdr/ |
| foaf:isPrimaryTopicOf | wikipedia-en:FDR_(software) |
| foaf:name | FDR FDR2 FDR3 FDR4 (en) |
| is dbo:wikiPageDisambiguates of | dbr:FDR_(disambiguation) |
| is dbo:wikiPageRedirects of | dbr:FDR2 dbr:Failures-Divergence_Refinement dbr:Failures-Divergences_Refinement |
| is dbo:wikiPageWikiLink of | dbr:FDR2 dbr:FDR_(disambiguation) dbr:Gavin_Lowe_(computer_scientist) dbr:Failures-Divergence_Refinement dbr:Failures-Divergences_Refinement |
| is foaf:primaryTopic of | wikipedia-en:FDR_(software) |
