{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:36:09Z","timestamp":1725510969676},"reference-count":22,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"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":[[2008,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            We describe our experiences in mechanising the specification, refinement, and proof of the\n            <jats:italic>Mondex Electronic Purse<\/jats:italic>\n            using the Z\/Eves theorem prover. We took a conservative approach and mechanised the original L\n            <jats:sc>a<\/jats:sc>\n            T\n            <jats:sub>E<\/jats:sub>\n            X sources without changing their technical content, except to correct errors. We found problems in the original specification and some missing invariants in the refinements. Based on these experiences, we present novel and detailed guidance on how to drive Z\/Eves successfully. The work contributes to the Repository for the Verified Software Grand Challenge.\n          <\/jats:p>","DOI":"10.1007\/s00165-007-0059-y","type":"journal-article","created":{"date-parts":[[2007,12,7]],"date-time":"2007-12-07T10:53:50Z","timestamp":1197024830000},"page":"117-139","source":"Crossref","is-referenced-by-count":24,"title":["Mechanising Mondex with Z\/Eves"],"prefix":"10.1145","volume":"20","author":[{"given":"Leo","family":"Freitas","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of York, YO10 5DD, Heslington, York, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jim","family":"Woodcock","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of York, YO10 5DD, Heslington, York, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"issue":"2","key":"e_1_2_1_2_1_2","first-page":"143","article-title":"The verified software repository: a step towards the verifying compiler","volume":"18","author":"Bicarregui J","year":"2006","journal-title":"FACJ"},{"key":"e_1_2_1_2_2_2","unstructured":"Cooper D Stepney S Woodcock J (2002) Derivation of Z Refinement Proof Rules. Technical Report YCS-2002-347 University of York"},{"key":"e_1_2_1_2_3_2","volume-title":"Practical elements of safety: proceedings of the 12th safety-critical systems symposium.","author":"Crocker D","year":"2004"},{"key":"e_1_2_1_2_4_2","unstructured":"Hung DV George C Janowski T Moore R (eds) (2002) Specification Case Studies in RAISE. FACIT (Formal Approaches to Computing and Information Technology) series. Springer Heidelberg"},{"key":"e_1_2_1_2_5_2","unstructured":"Information Technology\u2014Z Formal Specification Notation\u2014Syntax Type System and Semantics. ISO\/IEC 13568:2002(E) 2002"},{"key":"e_1_2_1_2_6_2","unstructured":"ITSEC. Information Technology Security Evaluation Criteria (ITSEC): Preliminary Harmonised Criteria. Document COM(90) 314 Version 1.2. Commission of the European Communities (1991)"},{"key":"e_1_2_1_2_7_2","volume-title":"Software Abstractions: Logic, Language, and Analysis pp 350","author":"Jackson D","year":"2006"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Jackson D (2006) Dependable software by design. Scientific American. June 2006","DOI":"10.1038\/scientificamerican0606-68"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.145"},{"key":"e_1_2_1_2_10_2","unstructured":"M\u00e9tayer C Abrial J-R Voisin L (2005) Event-B Language. Project IST-511599 RODIN Rigorous Open Development Environment for Complex Systems. RODIN Deliverable 3.2 Public Document. 31st May 2005 rodin.cs.ncl.ac.uk"},{"key":"e_1_2_1_2_11_2","volume-title":"Communicating and mobile systems: the \u03c0-calculus","author":"Milner R","year":"1999"},{"key":"e_1_2_1_2_12_2","unstructured":"Mondex smart cards. \nwww.mondex.com"},{"key":"e_1_2_1_2_13_2","unstructured":"The QPQ Deductive Software Repository. qpq.csl.sri.com"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Saaltink M (1997) The Z\/EVES User\u2019s Guide. ORA Canada","DOI":"10.1007\/BFb0027284"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Stepney S Cooper D Woodcock J (1998) More powerful Z data refinement: pushing the state of the art in industrial refinement. ZUM \u201998. Berlin Germany. LNCS vol 1493. Springer Heidelberg pp 284\u2013307","DOI":"10.1007\/978-3-540-49676-2_20"},{"key":"e_1_2_1_2_16_2","unstructured":"Stepney S Cooper D Woodcock J (2000) An electronic purse: specification refinement and proof. Technical monograph PRG-126 Oxford University Computing Laboratory. July 2000"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Schellhorn G Grandy H Haneberg D Reif W (2006) The Mondex challenge: machine checked proofs for an electronic purse. In: Misra J et\u00a0al (eds) FM 2006: formal methods 14th international symposium on formal methods Hamilton Canada August 21\u201327 2006. Springer Heidelberg pp 16\u201331","DOI":"10.1007\/11813040_2"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Schellhorn G Grandy H Haneberg D Reif W (2006) The Mondex challenge: machine checked proofs for an electronic purse. Technical Report. Institute of Computer Science University of Augsburg","DOI":"10.1007\/11813040_2"},{"key":"e_1_2_1_2_19_2","first-page":"150","volume-title":"The Z Notation: a reference manual","author":"Spivey JM","year":"1992","edition":"2"},{"key":"e_1_2_1_2_20_2","unstructured":"UML 2.0 OCL Specification. OMG Adopted Specification ptc\/03-10-14 2004"},{"key":"e_1_2_1_2_21_2","unstructured":"Woodcock J Davies J (1996) Using Z: Specification Refinement and Proof. Prentice Hall International Series in Computer Science 1996. pp 391. The complete text is available for free download from: www.usingz.com"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Woodcock J Stepney S Cooper D Clark J Jacob J (2008) The certification of the Mondex electronic purse to ITSEC Level E6. Formal Aspects Comput J 20(1) (this issue)","DOI":"10.1007\/s00165-007-0060-5"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-007-0059-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-007-0059-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-007-0059-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:49:22Z","timestamp":1641484162000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-007-0059-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,1]]},"references-count":22,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2008,1]]}},"alternative-id":["10.1007\/s00165-007-0059-y"],"URL":"https:\/\/doi.org\/10.1007\/s00165-007-0059-y","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,1]]}}}