{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T15:28:46Z","timestamp":1694618926102},"reference-count":9,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2000,12,1]],"date-time":"2000-12-01T00:00:00Z","timestamp":975628800000},"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":[[2000,12]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>This document gives a short overview of how VDMTools\u00ae can be used in different stages of the system\/software development process. The application used is a cash dispensing machine, first introduced at the FM'99 Symposium as the basis for a competition amongst tool vendors. The document provides an overview of how we at IFAD envisage that a problem such as this one should be attacked using VDMTools\u00ae.<\/jats:p>","DOI":"10.1007\/s001650070013","type":"journal-article","created":{"date-parts":[[2002,10,6]],"date-time":"2002-10-06T15:10:03Z","timestamp":1033917003000},"page":"216-217","source":"Crossref","is-referenced-by-count":0,"title":["Using VDMTools to Model and Validate the Cash Dispenser Example"],"prefix":"10.1145","volume":"12","author":[{"given":"Peter Gorm","family":"Larsen","sequence":"first","affiliation":[{"name":"IFAD A\/S, Odense, Denmark, , , , , , DK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paul","family":"Mukherjee","sequence":"additional","affiliation":[{"name":"IFAD A\/S, Odense, Denmark, , , , , , DK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kim","family":"Sunesen","sequence":"additional","affiliation":[{"name":"IFAD A\/S, Odense, Denmark, , , , , , DK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"issue":"9","key":"p_1","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1145\/185009.185028","volume":"29","author":"Elmstr\u00f8m R.","year":"1994","journal-title":"Formal Specifications. ACM Sigplan Notices"},{"key":"p_2","volume-title":"Modelling Systems - Practical Tools and Techniques in Software Development","author":"Fi","year":"1998"},{"key":"p_3","volume-title":"The Java Langauge Specification","author":"Gosling J.","year":"2000"},{"key":"p_4","volume-title":"IFAD","author":"[VDM00] The VDM Tool Group","year":"2000"},{"key":"p_5","volume-title":"Systematic Software Development Using VDM","author":"Jon","year":"1990"},{"key":"p_6","first-page":"133","volume-title":"Software Engineering Journal","author":"Muk","year":"1995"},{"key":"p_7","volume-title":"OMG","author":"The Common Object Request","year":"1996"},{"key":"p_8","volume-title":"December","author":"Larsen P. G.","year":"1996"},{"key":"p_9","unstructured":"[RSC00] Rational Software Corporation http:\/\/www.rational.com\/rose. Rational Rose 2000 Using Rose."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s001650070013.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s001650070013\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s001650070013","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:40:42Z","timestamp":1641483642000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s001650070013"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,12]]},"references-count":9,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2000,12]]}},"alternative-id":["10.1007\/s001650070013"],"URL":"https:\/\/doi.org\/10.1007\/s001650070013","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000,12]]}}}