{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:28Z","timestamp":1761611188159},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2006,9,1]],"date-time":"2006-09-01T00:00:00Z","timestamp":1157068800000},"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":[[2006,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>In this paper, we consider how refinements between state-based specifications (e.g., written in Z) can be checked by use of a model checker. Specifically, we are interested in the verification of downward and upward simulations which are the standard approach to verifying refinements in state-based notations. We show how downward and upward simulations can be checked using existing temporal logic model checkers.<\/jats:p>\n          <jats:p>In particular, we show how the branching time temporal logic CTL can be used to encode the standard simulation conditions. We do this for both a blocking, or guarded, interpretation of operations (often used when specifying reactive systems) as well as the more common non-blocking interpretation of operations used in many state-based specification languages (for modelling sequential systems). The approach is general enough to use with any state-based specification language, and we illustrate how refinements between Z specifications can be checked using the SAL CTL model checker using a small example.<\/jats:p>","DOI":"10.1007\/s00165-006-0002-7","type":"journal-article","created":{"date-parts":[[2006,8,7]],"date-time":"2006-08-07T11:56:51Z","timestamp":1154951811000},"page":"264-287","source":"Crossref","is-referenced-by-count":14,"title":["Verifying data refinements using a model checker"],"prefix":"10.1145","volume":"18","author":[{"given":"Graeme","family":"Smith","sequence":"first","affiliation":[{"name":"School of Information Technology and Electrical Engineering, The University of Queensland, 4072, Brisbane, Australia"}]},{"given":"John","family":"Derrick","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Sheffield, S1 4DP, Sheffield, UK"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Bolton C Davies J (2006) A singleton failures semantics for communicating sequential processes. Form Asp Comput (To appear)","DOI":"10.1007\/s00165-005-0081-x"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.04.023"},{"key":"e_1_2_1_2_3_2","volume-title":"International conference on computer aided verification (CAV\u201999), vol 1633 of LNCS","author":"Cimatti A","year":"1999"},{"key":"e_1_2_1_2_4_2","first-page":"154","volume-title":"International conference on computer aided verification (CAV\u201900), vol 1855 of LNCS","author":"Clarke E","year":"2000"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.5555\/332656"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.345825"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.5555\/379171"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-003-0007-4"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"de Roever W-P Engelhardt K (1998) Data refinement: model-oriented proof methods and their comparison. CUP","DOI":"10.1017\/CBO9780511663079"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"de Moura L Owre S Rue\u00df H Rushby J Shankar N Sorea M Tiwari A (2004) SAL 2. In: Alur R Peled D (eds) International conference on computer aided verification (CAV 2004) vol 3114 of LNCS. Springer Berlin Heidelberg New York pp 496\u2013500","DOI":"10.1007\/978-3-540-27813-9_45"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"de Moura L Owre S Shankar N (2003) The SAL language manual. Technical Report SRI-CSL-01-02 (Rev.2) SRI International","DOI":"10.1007\/978-3-540-27813-9_45"},{"key":"e_1_2_1_2_12_2","first-page":"996","volume-title":"Handbook of Theoretical Computer Science, vol B","author":"Emerson EA","year":"1990"},{"key":"e_1_2_1_2_13_2","first-page":"315","volume-title":"International conference on integrated formal methods (IFM\u201999)","author":"Fischer C","year":"1999"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Graf S Sa\u00efdi H (1997) Construction of abstract state graphs with PVS. In: International Conference on Computer Aided Verification (CAV\u201997) vol 1254 of LNCS. Springer Berlin Heidelberg New York pp 72\u201383","DOI":"10.1007\/3-540-63166-6_10"},{"key":"e_1_2_1_2_15_2","unstructured":"He J (1989) Process refinement. In: McDermid J (ed) The theory and practice of refinement. Butterworths London"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01788563"},{"key":"e_1_2_1_2_17_2","unstructured":"Kassel G Smith G (2001) Model checking Object-Z classes: some experiments with FDR. In: Asia-Pacific Software Engineering Conference (APSEC 2001). IEEE Computer Society Press Los Alamitor"},{"key":"e_1_2_1_2_18_2","first-page":"345","volume-title":"International conference on formal engineering methods, ICFEM 2005, vol 3785 of LNCS","author":"Leuschel M","year":"2005"},{"key":"e_1_2_1_2_19_2","first-page":"99","volume-title":"FME, vol 2021 of LNCS","author":"Leuschel M","year":"2001"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(00)00023-X"},{"key":"e_1_2_1_2_21_2","first-page":"62","volume-title":"International Conference of Z and B Users (ZB 2002), vol 2272 of LNCS","author":"Robinson N","year":"2002"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-005-0065-x"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011269103179"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Smith G (2000) The Object-Z Specification Language. Advances in Formal Methods. Kluwer","DOI":"10.1007\/978-1-4615-5265-9"},{"key":"e_1_2_1_2_25_2","unstructured":"Spivey JM (1992) The Z Notation: A reference manual. Prentice Hall 2nd edn"},{"key":"e_1_2_1_2_26_2","first-page":"443","volume-title":"International conference on computer aided verification (CAV\u201999), vol 1633 of LNCS","author":"Sa\u00efdi H","year":"1999"},{"key":"e_1_2_1_2_27_2","first-page":"260","volume-title":"International conference of Z and B users (ZB 2003), vol 2651 of LNCS","author":"Smith G","year":"2003"},{"key":"e_1_2_1_2_28_2","first-page":"87","volume-title":"International conference of Z and B users (ZB 2005), vol 3455 of LNCS","author":"Smith G","year":"2005"},{"key":"e_1_2_1_2_29_2","volume-title":"Using Z: specification, refinement, and proof","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-006-0002-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-006-0002-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-006-0002-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:49:25Z","timestamp":1641484165000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-006-0002-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,9]]},"references-count":29,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2006,9]]}},"alternative-id":["10.1007\/s00165-006-0002-7"],"URL":"https:\/\/doi.org\/10.1007\/s00165-006-0002-7","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,9]]}}}