| 词条 | FDR (software) |
| 释义 |
| name = FDR | logo = FDR4_CSP_refinement_checker_software_logo.png | logo alt = | logo caption = | screenshot = | screenshot alt = | caption = | collapsible = | author = | developer = University of Oxford | released = | discontinued = | ver layout = | latest release version = 4.2.0 | latest release date = {{Start date and age|2016|12|19|df=yes}} | latest preview version = | latest preview date = | status = | programming language = | operating system = {{Plainlist|
}} | platform = | size = | language = | language count = | language footnote = | genre = CSP refinement checker | license = proprietary software | alexa = | website = | repo = | standard = | AsOf = }}FDR (Failures-Divergences Refinement) and subsequently FDR2 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.[1] Bill Roscoe of the Department of Computer Science, University of Oxford devised many of the algorithms used by the tool and Michael Goldsmith[2] was instrumental in the implementation.[3] FDR2 is developed by Department of Computer Science, University of Oxford from where it is freely available for academic and other non-commercial use.[4] 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).[5] 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.[6] A ProBE CSP Animator is integrated in FDR3. It now has been succeeded by FDR4. References1. ^Formal Systems (Europe) Ltd. {{programming-software-stub}}2. ^[https://www.cs.ox.ac.uk/people/michael.goldsmith/ Professor Michael Goldsmith] (also now of Oxford University). 3. ^Philippa Broadfoot and Bill Roscoe. [https://books.google.com/books?id=Vl8YM4LJsacC&pg=PA322 Tutorial on FDR and Its Applications]. In Klaus Havelund, John Penix, Willem Visser (editors), [https://books.google.com/books?id=Vl8YM4LJsacC SPIN model checking and software verification], Springer-Verlag, Lecture Notes in Computer Science, Volume 1885, page 322, 2000. 4. ^Software: FDR2, with commercial licences obtainable from Formal Systems (Europe) Ltd. 5. ^{{cite paper|author=A.W. Roscoe|title=Model-checking CSP|version=In A Classical Mind: essays in Honour of C.A.R. Hoare|publisher=Prentice Hall|year=1994}} 6. ^[https://www.cs.ox.ac.uk/projects/fdr/manual/introduction.html Introduction to FDR3 ] 3 : Model checkers|Concurrent computing|Oxford University Computing Laboratory |
| 随便看 |
|
开放百科全书收录14589846条英语、德语、日语等多语种百科知识，基本涵盖了大多数领域的百科知识，是一部内容自由、开放的电子版国际百科全书。