{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T10:15:35Z","timestamp":1772532935304,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540627173","type":"print"},{"value":"9783540684909","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0027283","type":"book-chapter","created":{"date-parts":[[2005,11,19]],"date-time":"2005-11-19T07:00:45Z","timestamp":1132383645000},"page":"52-71","source":"Crossref","is-referenced-by-count":34,"title":["Automating test case generation from Z specifications with Isabelle"],"prefix":"10.1007","author":[{"given":"Steffen","family":"Helke","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Neustupny","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Santen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,17]]},"reference":[{"key":"4_CR1","unstructured":"J. P. Bowen and J. A. Hall, editors. Z User Workshop, Workshops in Computing. Springer Verlag, 1994."},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"J. P. Bowen and M. G. Hinchey, editors. ZUM'95: The Z Formal Specification Notation, LNCS 967. Springer Verlag, 1995.","DOI":"10.1007\/3-540-60271-2"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"R. B\u00fcssow and M. Weber. A Steam-Boiler Control Specification using Statecharts and Z. In J. R. Abrial, editor, Formal methods for industrial applications: specifying and programming the Steam Boiler Control, LNCS 1165. Springer Verlag, 1996.","DOI":"10.1007\/BFb0027252"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"E. Cusack and G. H. B. Rafsanjani. ZEST. In S. Stepney, R. Barden, and D. Cooper, editors, Object-Orientation in Z, Workshops in Computing. Springer Verlag, 1992.","DOI":"10.1007\/978-1-4471-3552-4_10"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"J. Dick and A. Faivre. Automating the generation and sequencing of test cases from model-based specifications. In Woodcock and Larsen [17], pages 268\u2013284.","DOI":"10.1007\/BFb0024651"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"M.-C. Gaudel. Testing can be formal, too. In P. D. Mosses, M. Nielsen, and M. I. Schwartzbach, editors, TAPSOFT '95: Theory and Practice of Software Development, LNCS 915, pages 82\u201396. Springer Verlag, 1995.","DOI":"10.1007\/3-540-59293-8_188"},{"key":"4_CR7","unstructured":"M. J. C. Gordon and T. M. Melham. Introduction to HOL: A theorem proving environment for higher order logics. Cambridge University Press, 1993."},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"H.-M. H\u00f6rcher. Improving software tests using Z specifications. In Bowen and Hinchey [2], pages 152\u2013166.","DOI":"10.1007\/3-540-60271-2_118"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Kolyang, T. Santen, and B. Wolff. A structure preserving encoding of Z in Isabelle\/HOL. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher-Order Logics, LNCS 1125, pages 283\u2013298. Springer Verlag, 1996.","DOI":"10.1007\/BFb0105411"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"E. Mikk. Compilation of Z specifications into C for automatic test result evaluation. In Bowen and Hinchey [2], pages 167\u2013180.","DOI":"10.1007\/3-540-60271-2_119"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"J. Nicholls. Z Notation \u2014 version 1.2. Draft ISO standard, 1995.","DOI":"10.21236\/ADA388235"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Isabelle \u2014 A Generic Theorem Prover. LNCS 828. Springer Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"4_CR13","unstructured":"H. Singh, M. Conrad, G. Egger, and S. Sadeghipour. Tool-supported test case design based on Z and the classification-tree method, 1996. Proc. Second Workshop on Systems for Computer-Aided Specification, Development and Verification, to appear."},{"key":"4_CR14","volume-title":"The","author":"J. M. Spivey","year":"1992","unstructured":"J. M. Spivey. The Fcuzz manual. Computing Science Consultancy, Oxford, UK, 1992."},{"key":"4_CR15","unstructured":"J. M. Spivey. The Z Notation \u2014 A Reference Manual. Prentice Hall, 2nd edition, 1992."},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"S. Stepney. Testing as abstraction. In Bowen and Hinchey [2], pages 137\u2013151.","DOI":"10.1007\/3-540-60271-2_117"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"J. C. P. Woodcock and P. G. Larsen, editors. FME '93: Industrial-Strength Formal Methods, LNCS 670. Springer Verlag, 1993.","DOI":"10.1007\/BFb0024633"}],"container-title":["Lecture Notes in Computer Science","ZUM '97: The Z Formal Specification Notation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0027283","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,5]],"date-time":"2023-05-05T14:01:24Z","timestamp":1683295284000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0027283"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540627173","9783540684909"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/bfb0027283","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997]]}}}