Mechanising Mondex with Z/Eves

citation_journal_title=FACJ; citation_title=The verified software repository: a step towards the verifying compiler; citation_author=J Bicarregui, T Hoare, J Woodcock; citation_volume=18; citation_issue=2; citation_publication_date=2006; citation_pages=143-151; citation_id=CR1 Cooper D, Stepney S, Woodcock J (2002) Derivation of Z Refinement Proof Rules. Technical Report YCS-2002-347, University of York citation_title=Safe object-oriented software: the verified design-by-contract paradigm; citation_inbook_title=Practical elements of safety: proceedings of the 12th safety-critical systems symposium.; citation_publication_date=2004; citation_id=CR3; citation_author=D Crocker; citation_publisher=Springer 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 Information Technology—Z Formal Specification Notation—Syntax, Type System and Semantics. ISO/IEC 13568:2002(E) 2002 ITSEC. Information Technology Security Evaluation Criteria (ITSEC): Preliminary Harmonised Criteria. Document COM(90) 314, Version 1.2. Commission of the European Communities (1991) citation_title=Software Abstractions: Logic, Language, and Analysis pp 350; citation_publication_date=2006; citation_id=CR7; citation_author=D Jackson; citation_publisher=The MIT Jackson D (2006) Dependable software by design. Scientific American. June 2006 citation_journal_title=IEEE Comput; citation_title=Verified software: a Grand Challenge; citation_author=C Jones, P O’Hearn, J Woodcock; citation_volume=39; citation_issue=4; citation_publication_date=2006; citation_pages=93-95; citation_id=CR9 Métayer 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 citation_title=Communicating and mobile systems: the π-calculus; citation_publication_date=1999; citation_id=CR11; citation_author=R Milner; citation_publisher=Cambridge University Press Mondex smart cards. www.mondex.com The QPQ Deductive Software Repository. qpq.csl.sri.com Saaltink M (1997) The Z/EVES User’s Guide. ORA Canada Stepney S, Cooper D, Woodcock J (1998) More powerful Z data refinement: pushing the state of the art in industrial refinement. ZUM ’98. Berlin, Germany. LNCS, vol 1493. Springer, Heidelberg, pp 284–307 Stepney S, Cooper D, Woodcock J (2000) An electronic purse: specification, refinement, and proof. Technical monograph PRG-126, Oxford University Computing Laboratory. July 2000 Schellhorn G, Grandy H, Haneberg D, Reif W (2006) The Mondex challenge: machine checked proofs for an electronic purse. In: Misra J et al (eds) FM 2006: formal methods, 14th international symposium on formal methods, Hamilton, Canada, August 21–27, 2006. Springer, Heidelberg, pp 16–31 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 citation_title=The Z Notation: a reference manual; citation_publication_date=1992; citation_id=CR19; citation_author=JM Spivey; citation_publisher=Prentice Hall International Series in Computer Science UML 2.0 OCL Specification. OMG Adopted Specification ptc/03-10-14 2004 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 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)