{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T14:48:26Z","timestamp":1725547706400},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642118104"},{"type":"electronic","value":"9783642118111"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11811-1_28","type":"book-chapter","created":{"date-parts":[[2010,2,19]],"date-time":"2010-02-19T11:57:22Z","timestamp":1266580642000},"page":"377-390","source":"Crossref","is-referenced-by-count":9,"title":["Translating Z to Alloy"],"prefix":"10.1007","author":[{"given":"Petra","family":"Malik","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lindsay","family":"Groves","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Clare","family":"Lenihan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"28_CR1","unstructured":"Arthan, R.: Proofpower, \n                    \n                      http:\/\/www.lemma-one.com\/ProofPower\/"},{"key":"28_CR2","series-title":"LNBIP","volume-title":"Proceedings of Objects, Components, Models and Patterns, 46th International Conference, TOOLS EUROPE 2008","author":"E.G. Aydal","year":"2008","unstructured":"Aydal, E.G., Utting, M., Woodcock, J.: A comparison of state-based modelling tools for model validation. In: Proceedings of Objects, Components, Models and Patterns, 46th International Conference, TOOLS EUROPE 2008, Zurich, Switzerland, June 30 - July 4, 2008. LNBIP, vol.\u00a011. Springer, Heidelberg (2008)"},{"key":"28_CR3","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.entcs.2005.04.023","volume":"137","author":"C. Bolton","year":"2005","unstructured":"Bolton, C.: Using the Alloy analyzer to verify data refinement in Z. Electronic Notes in Theoretical Computer Science\u00a0137, 23\u201344 (2005)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"28_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Abstract State Machines, B and Z","year":"2008","unstructured":"B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.): ABZ 2008. LNCS, vol.\u00a05238. Springer, Heidelberg (2008)"},{"key":"28_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"678","DOI":"10.1007\/11901433_37","volume-title":"Formal Methods and Software Engineering, 8th International Conference on Formal Engineering Methods, ICFEM 2006","author":"J. Derrick","year":"2006","unstructured":"Derrick, J., North, S., Simons, T.: Issues in implementing a model checker for Z. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 678\u2013696. Springer, Heidelberg (2006)"},{"key":"28_CR6","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1016\/j.entcs.2008.06.015","volume":"214","author":"H.-C. Estler","year":"2008","unstructured":"Estler, H.-C., Wehrheim, H.: Alloy as a refactoring checker? Electronic Notes in Theoretical Computer Science\u00a0214, 331\u2013357 (2008)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"28_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/BFb0027282","volume-title":"ZUM\u201997: The Z Formal Specification Notation","author":"M.A. Hewitt","year":"1997","unstructured":"Hewitt, M.A., O\u2019Halloran, C.M., Sennett, C.T.: Experiences with PiZA, an animator for Z. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol.\u00a01212, pp. 37\u201351. Springer, Heidelberg (1997)"},{"key":"#cr-split#-28_CR8.1","unstructured":"ISO\/IEC 13568. Information Technology\u2014Z Formal Specification Notation\u2014Syntax, Type System and Semantics. ISO\/IEC (2002);"},{"key":"#cr-split#-28_CR8.2","unstructured":"First Edition 2002-07-01"},{"key":"28_CR9","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D. Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge (2006)"},{"key":"28_CR10","doi-asserted-by":"crossref","unstructured":"Kang, E., Jackson, D.: Formal modeling and analysis of a flash filesystem in Alloy. In: B\u00f6rger, et al. (eds.) [4], pp. 294\u2013308","DOI":"10.1007\/978-3-540-87603-8_23"},{"issue":"2","key":"28_CR11","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M. Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf.\u00a010(2), 185\u2013203 (2008)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"28_CR12","doi-asserted-by":"crossref","unstructured":"Malik, P., Utting, M.: CZT: A framework for Z tools. In: Treharne, et al. (eds.) [21], pp. 65\u201384","DOI":"10.1007\/11415787_5"},{"key":"28_CR13","doi-asserted-by":"crossref","unstructured":"ORA Canada. Z\/EVES version 1.5: An overview. In: Hutter, D., Traverso, P. (eds.) FM-Trends 1998. LNCS, vol.\u00a01641, pp. 367\u2013376. Springer, Heidelberg (1999)","DOI":"10.1007\/3-540-48257-1_28"},{"key":"28_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/978-3-540-73210-5_25","volume-title":"Integrated Formal Methods","author":"D. Plagge","year":"2007","unstructured":"Plagge, D., Leuschel, M.: Validating Z specifications using the ProB animator and model checker. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol.\u00a04591, pp. 480\u2013500. Springer, Heidelberg (2007)"},{"issue":"1","key":"28_CR15","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s00165-007-0058-z","volume":"20","author":"T. Ramananandro","year":"2008","unstructured":"Ramananandro, T.: Mondex, an electronic purse: specification and refinement checks with the Alloy model-finding method. Formal Aspects of Computing\u00a020(1), 21\u201339 (2008)","journal-title":"Formal Aspects of Computing"},{"key":"28_CR16","unstructured":"Reeve, G., Reeves, S.: Experiences using Z animation tools. Technical Report 01\/3\/2001, Department of Computer Science, University of Waikato (2001)"},{"key":"28_CR17","doi-asserted-by":"crossref","unstructured":"Smith, G., Wildman, L.: Model checking Z specifications using SAL. In: Treharne, et al. (eds.) [21]","DOI":"10.1007\/11415787_6"},{"key":"28_CR18","volume-title":"The Z Notation: A Reference Manual","author":"J.M. Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual. Prentice Hall International (UK) Ltd., Hertfordshire (1992)"},{"key":"28_CR19","unstructured":"Spivey, M.: The fuzz type-checker for Z, \n                    \n                      http:\/\/spivey.oriel.ox.ac.uk\/mike\/fuzz\/"},{"key":"28_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 632\u2013647. Springer, Heidelberg (2007)"},{"key":"28_CR21","series-title":"Lecture Notes in Computer Science","volume-title":"ZB 2005: Formal Specification and Development in Z and B","year":"2005","unstructured":"Treharne, H., King, S., Henson, M.C., Schneider, S. (eds.): ZB 2005. LNCS, vol.\u00a03455. Springer, Heidelberg (2005)"},{"key":"28_CR22","doi-asserted-by":"crossref","unstructured":"Utting, M., Malik, P.: Unit testing of Z specifications. In: B\u00f6rger, et al. (eds.) [4], pp. 309\u2013322","DOI":"10.1007\/978-3-540-87603-8_24"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B and Z"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11811-1_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:44:16Z","timestamp":1606185856000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11811-1_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642118104","9783642118111"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11811-1_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}