{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T19:00:23Z","timestamp":1694631623018},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"1-2","license":[{"start":{"date-parts":[[2009,2,1]],"date-time":"2009-02-01T00:00:00Z","timestamp":1233446400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2009,2]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We describe: (1) the internal structures of FDR, the refinement model checker for Hoare\u2019s Communicating Sequential Processes (CSP); and (2) an application-programming interface (API) that allows users to interact more closely with FDR and to have finer-grain control over its behaviour and data structures. This API makes it possible to create optimised CSP code to perform refinement checks that are more space or time efficient, enabling the analysis of more complex and data-intensive specifications. The API can be used either by those constructing CSP models or by tools that automatically generate CSP code. We present examples of using our tool, including handling advanced FDR features such as transparent functions, which compress state spaces before checking. We also show how to transform FDR\u2019s graph format into a graph notation such as JGraph, enabling visualisation of labelled transition systems of CSP specifications.<\/jats:p>","DOI":"10.1007\/s00165-008-0074-7","type":"journal-article","created":{"date-parts":[[2008,4,2]],"date-time":"2008-04-02T08:55:24Z","timestamp":1207126524000},"page":"133-154","source":"Crossref","is-referenced-by-count":3,"title":["FDR Explorer"],"prefix":"10.1145","volume":"21","author":[{"given":"Leo","family":"Freitas","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of York, YO10 5DD, York, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jim","family":"Woodcock","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of York, YO10 5DD, York, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","volume-title":"Interacting with the CSP compiler","author":"Armstrong P","year":"2007"},{"issue":"2","key":"e_1_2_1_2_2_2","first-page":"143","article-title":"The verified software repository: a step towards the verifying compiler","volume":"18","author":"Bicarregui J","year":"2006","journal-title":"FACJ"},{"key":"e_1_2_1_2_3_2","unstructured":"Cabral G Sampaio A (2006) Formal specification generation from requirement documents. In: Brazilian symposium in formal methods SBMF."},{"issue":"1","key":"e_1_2_1_2_4_2","first-page":"1","article-title":"Testing equivalence as a bisimulation equivalence","volume":"5","author":"Cleaveland R","year":"1993","journal-title":"FACJ"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/242223.242257"},{"key":"e_1_2_1_2_6_2","unstructured":"Freitas L (2005) Model Checking Circus. PhD Thesis University of York"},{"key":"e_1_2_1_2_7_2","unstructured":"Freitas L (2007) FDR Explorer v0.4. http:\/\/www.cs.york.ac.uk\/~leo"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Freitas L Cavalcanti A Woodcock J (2006) Taking our own medicine: applying the refinement calculus to the development of a model checker. Formal Methods and Software Engineering (8th ICFEM) LNCS 4260 pp 697\u2013716","DOI":"10.1007\/11901433_38"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-006-0021-9"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Goldsmith M Moffat N Roscoe B Whitworth T Zakiuddin I (2003) Watchdog transformations for property-oriented model-checking. In: Proceedings of the 12st international FME symposium Pisa Italy. LNCS 2805 pp 600\u2013616. Springer Heidelberg","DOI":"10.1007\/978-3-540-45236-2_33"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Goldsmith M (2004) Operational semantics for fun and profit. In: The first 25\u00a0years of communicating sequential processes London UK. LNCS 3525 pp 265\u2013274. Springer Heidelberg","DOI":"10.1007\/11423348_16"},{"key":"e_1_2_1_2_12_2","unstructured":"Goldsmith M (2005) FDR2 user\u2019s manual version 2.82 Formal Systems (Europe) Ltd"},{"key":"e_1_2_1_2_13_2","unstructured":"JGraph user\u2019s manual (2006) http:\/\/www.jgraph.com\/pub\/jgraphmanual.pdf"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Lawrence J (2004) Practical application of CSP and FDR to software design. In: Abdallah AE Jones C Sanders J (eds) 25\u00a0years of CSP FACJ","DOI":"10.1007\/11423348_9"},{"key":"e_1_2_1_2_15_2","volume-title":"Casper user manual","author":"Lowe G","year":"1997"},{"key":"e_1_2_1_2_16_2","unstructured":"Martin J Duddart Y (2000) Parallel algorithms for deadlock and livelock analysis of concurrent systems. In: Welch P Bakkers A (eds) Communicating process architectures. IOS Press pp 1\u201314"},{"key":"e_1_2_1_2_17_2","unstructured":"Martin J (1996) The design and construction of deadlock-free concurrent systems. PhD Thesis University of Buckingham"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00245458"},{"key":"e_1_2_1_2_19_2","unstructured":"Roscoe B Gardiner P Goldsmith M Hulance J Jackson D Scattergood J (1995) Hierarchical compression for model checking CSP or how to check 10 20 dining philosophers for deadlock. First TACAS in LNCS Springer 1019(1)"},{"key":"e_1_2_1_2_20_2","unstructured":"Roscoe B (1995) Model checking CSP in a classical mind: essays in honour of C. A. R. Hoare. In: International series in computer science Chap. 21. Prentice-Hall Englewood Cliffs pp 353\u2013378"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.5555\/550448"},{"key":"e_1_2_1_2_22_2","volume-title":"Modelling and analysis of security protocols","author":"Ryan P","year":"2001"},{"key":"e_1_2_1_2_23_2","unstructured":"Scattergood J (1998) The semantics and implementation of machine readable CSP. PhD Thesis Oxford University The Queen\u2019s College"},{"key":"e_1_2_1_2_24_2","unstructured":"Srivatanakul T (2005) Security analysis with deviational techniques. PhD Thesis University of York"},{"key":"e_1_2_1_2_25_2","unstructured":"Tcl\/Tk: Tool command language 2006. http:\/\/www.tcl.tk\/"},{"key":"e_1_2_1_2_26_2","unstructured":"The test sequence generator TGV. http:\/\/www-verimag.imag.fr\/~async\/TGV"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Valmari A (1990) A stubborn attack on state explosion. In: Proceedings of 2nd international conference in computer-aided verification. LNCS 531. Springer Heidelberg pp 156\u2013165","DOI":"10.1007\/BFb0023729"},{"key":"e_1_2_1_2_28_2","volume-title":"Using Z: Specification, refinement, and proof. International series in computer science","author":"Woodcock J","year":"1996"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-008-0074-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-008-0074-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-008-0074-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:47:27Z","timestamp":1641484047000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-008-0074-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,2]]},"references-count":28,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2009,2]]}},"alternative-id":["10.1007\/s00165-008-0074-7"],"URL":"https:\/\/doi.org\/10.1007\/s00165-008-0074-7","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,2]]}}}