{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,24]],"date-time":"2025-05-24T07:40:10Z","timestamp":1748072410162,"version":"3.41.0"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Automated Software Engineering"],"published-print":{"date-parts":[[1997,1]]},"DOI":"10.1023\/a:1008603612253","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T15:12:40Z","timestamp":1040569960000},"page":"33-51","source":"Crossref","is-referenced-by-count":4,"title":["Specification and Animation of a Bank Transfer using KIDS\/VDM"],"prefix":"10.1007","volume":"4","author":[{"given":"Yves","family":"Ledru","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"125024_CR1","unstructured":"Andrews, D., Bruun, H., Hansen, B., Larsen, P., Plat, N. et al. 1995, Information Technology\u2014Programming Languages, their environments and system software interfaces\u2014Vienna Development Method-Specification Language Part 1: Base language, ISO."},{"key":"125024_CR2","unstructured":"Barclays Bank PLC,. 1991, The Barclays code of business banking, Barclays Bank, Commercial Banking Division."},{"key":"125024_CR3","doi-asserted-by":"crossref","unstructured":"Bicarregui, J. C., Fitzgerald, J. S., Lindsay, P. A., Moore, R. and Ritchie, B. 1994, Proof in VDM: A Practitioner's Guide, FACIT, Springer-Verlag.","DOI":"10.1007\/978-1-4471-2033-9"},{"key":"125024_CR4","doi-asserted-by":"crossref","unstructured":"Bowen, J. and Stavridou, V. 1992, Safety-critical systems, formal methods and standards, Technical Report PRG-TR-5-92, Oxford University Computing Laboratory.","DOI":"10.1016\/B978-0-08-041893-3.50020-3"},{"key":"125024_CR5","unstructured":"Chung, L., Nixon, B. and Yu, E. 1995, Using non-functional requirements to systematically support change, RE '95-Second IEEE international symposium on Requirements Engineering."},{"key":"125024_CR6","unstructured":"Craigen, D., Gerhart, S. and Ralston, T. 1993, An international survey of industrial applications of formal methods, Technical Report NISTGCR 93\/626, U.S. National Institute of Standards and technology."},{"issue":"9","key":"125024_CR7","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1145\/185009.185028","volume":"29","author":"R. Elmstrom","year":"1994","unstructured":"Elmstrom, R., Larsen, P. G. and Lassen, P. B. 1994, The IFAD VDM-SL toolbox: a practical approach to formal specifications, ACM SIGPLAN Notices\n29(9), 77-80.","journal-title":"ACM SIGPLAN Notices"},{"issue":"6","key":"125024_CR8","first-page":"320","volume":"4","author":"I. J. Hayes","year":"1989","unstructured":"Hayes, I. J. and Jones, C. B. 1989, Specifications are not (necessarily) executable, IEE, Software Engineering Journal\n4(6), 320-338.","journal-title":"IEE, Software Engineering Journal"},{"key":"125024_CR9","unstructured":"Hekmatpour, S. and Ince, D. 1988, Software prototyping, formal methods and VDM, Addison-Wesley."},{"issue":"2","key":"125024_CR10","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1109\/TSE.1986.6312939","volume":"12","author":"P. Henderson","year":"1986","unstructured":"Henderson, P. 1986, Functional programming, formal specification, and rapid prototyping, IEEE Transactions on Software Engineering\n12(2), 241-250.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"125024_CR11","volume-title":"Systematic Software Development Using VDM","author":"C. B. Jones","year":"1990","unstructured":"Jones, C. B. 1990, Systematic Software Development Using VDM (Secon Edition), Prentice-Hall, London.","edition":"Secon Edition"},{"key":"125024_CR12","doi-asserted-by":"crossref","unstructured":"Jones, C., Jones, K., Lindsay, P. and Moore, R. 1991, Mural: A Formal Development Support System, Springer-Verlag.","DOI":"10.1007\/978-1-4471-3180-9"},{"issue":"1","key":"125024_CR13","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1145\/181577.181582","volume":"29","author":"A. Kans","year":"1994","unstructured":"Kans, A. and Hayton, C. 1994, Using ABC to prototype VDM specifications, ACM SIGPLAN Notices\n29(1), 27-37.","journal-title":"ACM SIGPLAN Notices"},{"issue":"5","key":"125024_CR14","doi-asserted-by":"crossref","first-page":"565","DOI":"10.1007\/BF01211868","volume":"6","author":"P. G. Larsen","year":"1994","unstructured":"Larsen, P. G. 1994, Response to \u201dthe formal specification of safety requirements for storing explosives\u201d, Formal Aspects of Computing\n6(5), 565-568.","journal-title":"Formal Aspects of Computing"},{"key":"125024_CR15","doi-asserted-by":"crossref","unstructured":"Ledru, Y. 1994, Proof-based development of specifications with KIDS\/VDM, in M. Naftalin, T. Denvir and M. Bertran (eds), FME'94: Industrial Benefit of Formal Methods, Vol. 873 of Lecture Notes in Computer Science, Springer-Verlag, pp. 214-232.","DOI":"10.1007\/3-540-58555-9_97"},{"key":"125024_CR16","unstructured":"Ledru, Y. 1996, Using KIDS as a tool support for VDM, Proceedings of the 18th International Conference on Software Engineering, IEEE Computer Society Press."},{"key":"125024_CR17","unstructured":"Ledru, Y. and Li\u00e9geois, M.-H. 1991, Integrating REFINE prototypes in a VDM development framework, in B. M\u00f6ller (ed.), Proceedings of the IFIP TC2 Working conference on Constructing Programs from Specifications, North-Holland, pp. 243-265."},{"key":"125024_CR18","doi-asserted-by":"crossref","unstructured":"Ledru, Y. and Li\u00e9geois, M.-H. 1992, Prototyping VDM specifications with KIDS, Proceedings of the 7th Knowledge-Based Software Engineering Conference, IEEE Computer Society Press, pp. 50-59.","DOI":"10.1109\/KBSE.1992.252909"},{"key":"125024_CR19","doi-asserted-by":"crossref","unstructured":"Mukherjee, P. 1995, Computer-aided validation of formal specifications, IEE, Software Engineering Journal pp. 133-140.","DOI":"10.1049\/sej.1995.0017"},{"issue":"9","key":"125024_CR20","doi-asserted-by":"crossref","first-page":"1024","DOI":"10.1109\/32.58788","volume":"16","author":"D. Smith","year":"1990","unstructured":"Smith, D. 1990, KIDS: a semi-automatic program development system, IEEE Transactions on Software Engineering\u2014Special Issue on formal Methods\n16(9), 1024-1043.","journal-title":"IEEE Transactions on Software Engineering\u2014Special Issue on formal Methods"},{"issue":"11","key":"125024_CR21","doi-asserted-by":"crossref","first-page":"1278","DOI":"10.1109\/TSE.1985.231879","volume":"11","author":"D. Smith","year":"1985","unstructured":"Smith, D., Kotik, G. and Westfold, S. 1985, Research on Knowledge-Based Software Environments at Kestrel Institute, IEEE Transactions on Software Engineering\n11(11), 1278-1295.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"125024_CR22","unstructured":"Spivey, J. 1992, The Z notation-A Reference Manual (Second Edition), Prentice Hall."},{"key":"125024_CR23","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/0164-1212(89)90061-7","volume":"10","author":"R. B. Terwilliger","year":"1989","unstructured":"Terwilliger, R. B. and Campbell, R. H. 1989, ENCOMPASS: An environment for the incremental development of software, The Journal of Systems and Software\n10, 41-53.","journal-title":"The Journal of Systems and Software"}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008603612253.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008603612253\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008603612253.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,24]],"date-time":"2025-05-24T07:05:55Z","timestamp":1748070355000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008603612253"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,1]]},"references-count":23,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1997,1]]}},"alternative-id":["125024"],"URL":"https:\/\/doi.org\/10.1023\/a:1008603612253","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"type":"print","value":"0928-8910"},{"type":"electronic","value":"1573-7535"}],"subject":[],"published":{"date-parts":[[1997,1]]}}}