{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:42Z","timestamp":1761611202677},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2007,3,7]],"date-time":"2007-03-07T00:00:00Z","timestamp":1173225600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2007,3,27]]},"DOI":"10.1007\/s00236-007-0042-3","type":"journal-article","created":{"date-parts":[[2007,3,6]],"date-time":"2007-03-06T16:49:23Z","timestamp":1173199763000},"page":"41-71","source":"Crossref","is-referenced-by-count":6,"title":["On using data abstractions for model checking refinements"],"prefix":"10.1007","volume":"44","author":[{"given":"John","family":"Derrick","sequence":"first","affiliation":[]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2007,3,7]]},"reference":[{"key":"42_CR1","unstructured":"Boiten, E.A., Derrick, J.: IO-refinement in Z. In: Evans, A., Duke, D.J., Clark, T. (eds.) 3rd BCS-FACS Northern Formal Methods Workshop. Springer, Heidelberg (1998). http:\/\/www.ewic. org.uk\/"},{"key":"42_CR2","unstructured":"Bolton, C.: On the refinement of state-based and event-based models. PhD Thesis, University of Oxford (2002)"},{"key":"42_CR3","doi-asserted-by":"crossref","unstructured":"Bolton, C.: Using the alloy analyzer to verify data refinement in Z. In: Refine 2005. Electronic Notes in Theoretical Computer Science (2005)","DOI":"10.1016\/j.entcs.2005.04.023"},{"key":"42_CR4","doi-asserted-by":"crossref","unstructured":"Bolton, C., Davies, J.: Refinement in object-Z and CSP. In: Butler, M., Petre, L., Sere, K. (eds.) Integrated Formal Methods (IFM 2002). Lecture Notes in Computer Science, vol. 2335, pp. 225\u2013244. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-47884-1_13"},{"key":"42_CR5","doi-asserted-by":"crossref","unstructured":"Bolton, C., Davies, J.: A singleton failures semantics for communicating sequential processes. Form. Asp. Comput. (2006, to appear)","DOI":"10.1007\/s00165-005-0081-x"},{"issue":"3","key":"42_CR6","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1016\/j.tcs.2004.10.004","volume":"330","author":"C. Bolton","year":"2005","unstructured":"Bolton C. and Lowe G. (2005). A hierarchy of failures-based models: Theory and application. Theor. Comput. Sci. 330(3): 407\u2013438","journal-title":"Theor. Comput. Sci."},{"key":"42_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. In: 19th ACM POPL (1992)","DOI":"10.1145\/143165.143235"},{"issue":"5","key":"42_CR8","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E.M. Clarke","year":"2003","unstructured":"Clarke E.M., Grumberg O., Jha S., Lu Y. and Veith H. (2003). Counterexample-guided abstraction refinement for symbolic model checking. JACM 50(5): 752\u2013794","journal-title":"JACM"},{"key":"42_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P.: Abstract interpretation. ACM Comput. Surv. 28(2) (1996)","DOI":"10.1145\/234528.234740"},{"key":"42_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th ACM POPL (1977)","DOI":"10.1145\/512950.512973"},{"key":"42_CR11","unstructured":"Dams, D., Grumberg, O., Gerth, R.: Abstract interpretation of reactive systems: abstractions preserving \u2200 CTL *, \u2203 CTL * and CTL *. In: Olderog, E.-R. (ed.) Programming Concepts, Methods and Calculi, vol. A-56, pp. 573\u2013592. Elsevier, Amsterdam (1994)"},{"key":"42_CR12","doi-asserted-by":"crossref","first-page":"917","DOI":"10.1016\/S0950-5849(99)00044-0","volume":"41","author":"J. Derrick","year":"1999","unstructured":"Derrick J. and Boiten E.A. (1999). Calculating upward and downward simulations of state-based specifications. Inf. Softw. Technol. 41: 917\u2013923","journal-title":"Inf. Softw. Technol."},{"key":"42_CR13","doi-asserted-by":"crossref","unstructured":"Derrick, J., Boiten, E.A.: Refinement in Z and object-Z. Springer, Heidelberg (2001)","DOI":"10.1007\/978-1-4471-0257-1"},{"issue":"1","key":"42_CR14","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1007\/s00165-003-0007-4","volume":"15","author":"J. Derrick","year":"2003","unstructured":"Derrick J. and Boiten E.A. (2003). Relational concurrent refinement. Formal Aspects of Computing 15(1): 182\u2013214","journal-title":"Formal Aspects of Computing"},{"key":"42_CR15","doi-asserted-by":"crossref","unstructured":"de Roever, W.-P., Engelhardt, K.: Data refinement: model-oriented proof methods and their comparison. CUP (1998)","DOI":"10.1017\/CBO9780511663079"},{"key":"42_CR16","doi-asserted-by":"crossref","unstructured":"Farias, A., Mota, A., Sampaio, A.: Efficient CSPZ data abstraction. In: Integrated Formal Methods (IFM 2004). LNCS, vol. 2966, pp. 108\u2013127 (2004)","DOI":"10.1007\/978-3-540-24756-2_7"},{"key":"42_CR17","doi-asserted-by":"crossref","unstructured":"Fischer, C., Wehrheim, H.: Model-checking CSP-OZ specifications with FDR. In: Araki, K., Galloway, A., Taguchi, K. (eds.) Proceedings of the 1st International Conference on Integrated Formal Methods (IFM), pp. 315\u2013334. Springer, Heidelberg (1999)","DOI":"10.1007\/978-1-4471-0851-1_17"},{"key":"42_CR18","unstructured":"Formal Systems (Europe) Ltd. Failures-divergence refinement: FDR2 user manual (1997)"},{"key":"42_CR19","unstructured":"He, J.: Process refinement. In: McDermid, J. (ed.) The Theory and Practice of Refinement. Butterworths (1989)"},{"key":"42_CR20","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)"},{"key":"42_CR21","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/BF01788563","volume":"3","author":"M.B. Josephs","year":"1988","unstructured":"Josephs M.B. (1988). A state-based approach to communicating processes.. Distrib. Comput. 3: 9\u201318","journal-title":"Distrib. Comput."},{"key":"42_CR22","unstructured":"Kassel, G., Smith, G.: Model checking object-Z classes: some experiments with FDR. In: Asia-Pacific Software Engineering Conference (APSEC 2001). IEEE Computer Society Press (2001)"},{"key":"42_CR23","unstructured":"Lazic, R.: A semantic study of data independence with applications to model checking. PhD Thesis, Oxford University Computing Laboratory (1999)"},{"key":"42_CR24","unstructured":"Lazic, R., Roscoe, A.W.: Data independence with generalised predicate symbols. In: Parallel and Distributed Processing Techniques and Applications (PDPTA), pp. 319\u2013325. CSREA Press (1999)"},{"key":"42_CR25","doi-asserted-by":"crossref","unstructured":"Leuschel, M, Butler, M.J.: Automatic refinement checking for B. In: Kung-Kiu Lau, Richard Banach (eds.) ICFEM. Lecture Notes in Computer Science, vol. 3785, pp. 345\u2013359. Springer, Heidelberg (2005)","DOI":"10.1007\/11576280_24"},{"key":"42_CR26","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"Loiseaux C., Graf S., Sifakis J., Bouajjani A. and Bensalem S. (1995). Property preserving abstractions for the verification of concurrent systems. Form. Methods Syst. Des. 6: 1\u201335","journal-title":"Form. Methods Syst. Des."},{"key":"42_CR27","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1016\/S0167-6423(00)00023-X","volume":"40","author":"A. Mota","year":"2001","unstructured":"Mota A. and Sampaio A. (2001). Model-checking CSP-Z: strategy, tool support and industrial application. Sci. Comput. Program. 40: 59\u201396","journal-title":"Sci. Comput. Program."},{"key":"42_CR28","doi-asserted-by":"crossref","unstructured":"Mota, A., Borba, P., Sampaio, A.: Mechanical abstraction of CSP-Z processes. In: Eriksson, L.-H., Lindsay, P. (eds.) Formal Methods Europe (FME\u20192002). LNCS, vol. 2391, pp. 163\u2013183. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-45614-7_10"},{"key":"42_CR29","unstructured":"Roscoe, A.W.: The theory and practice of concurrency (1998)"},{"key":"42_CR30","doi-asserted-by":"crossref","unstructured":"Saaltink, M.: The Z\/EVES system. In: ZUM \u201997. LNCS, vol. 1212, pp. 72\u201388. Springer, Heidelberg (1997)","DOI":"10.1007\/BFb0027284"},{"key":"42_CR31","unstructured":"Scattergood, J.B.: The semantics and implementation of machine-readable CSP. PhD Thesis, University of Oxford (1998)"},{"key":"42_CR32","unstructured":"Schneider, S.: Non-blocking data refinement and traces-divergences semantics. Technical report, University of Surrey (2005)"},{"key":"42_CR33","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1023\/A:1011269103179","volume":"18","author":"G. Smith","year":"2001","unstructured":"Smith G. and Derrick J. (2001). Specification, refinement and verification of concurrent systems\u2014an integration of Object-Z and CSP. Form. Methods Syst. Des. 18: 249\u2013284","journal-title":"Form. Methods Syst. Des."},{"key":"42_CR34","doi-asserted-by":"crossref","unstructured":"Smith, G., Derrick, J.: Model checking downward simulations. In: REFINE 2005, Electronic notes in theoretical computer science, vol. 137, pp. 205\u2013224 (2005)","DOI":"10.1016\/j.entcs.2005.04.032"},{"issue":"3","key":"42_CR35","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1007\/s00165-006-0002-7","volume":"18","author":"G. Smith","year":"2006","unstructured":"Smith G. and Derrick J. (2006). Verifying data refinements using a model checker. Form. Asp. Comput. 18(3): 264\u2013287","journal-title":"Form. Asp. Comput."},{"key":"42_CR36","doi-asserted-by":"crossref","unstructured":"Smith, G., Wildman, L.: Model checking Z specifications using SAL. In: International conference of B and Z users (ZB 2005). Lecture Notes in Computer Science, vol. 3455, pp. 85\u2013103. Springer, Heidelberg (2005)","DOI":"10.1007\/11415787_6"},{"key":"42_CR37","unstructured":"Spivey, J.M.: The Z notation: a reference manual, 2nd edn. Int. Ser. Comput. Sci. Prentice Hall, Englewood Cliffs (1992)"},{"key":"42_CR38","doi-asserted-by":"crossref","unstructured":"Stepney, S., Cooper, D., Woodcock, J.C.P.: More powerful data refinement in Z. In: Bowen, J.P., Fett, A., Hinchey, M.G. (eds.) ZUM\u201998: The Z Formal Specification Notation. Lecture Notes in Computer Science, vol. 1493, pp. 284\u2013307. Springer, Heidelberg (1998)","DOI":"10.1007\/978-3-540-49676-2_20"},{"key":"42_CR39","doi-asserted-by":"crossref","unstructured":"Wehrheim, H.: Data abstraction techniques in the validation of CSP-OZ specifications. Form. Asp. Comput. 12 (2000)","DOI":"10.1007\/s001650070026"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-007-0042-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-007-0042-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-007-0042-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,24]],"date-time":"2019-05-24T13:41:54Z","timestamp":1558705314000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-007-0042-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,3,7]]},"references-count":39,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,3,27]]}},"alternative-id":["42"],"URL":"https:\/\/doi.org\/10.1007\/s00236-007-0042-3","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,3,7]]}}}