{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:37:03Z","timestamp":1725543423284},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642114465"},{"type":"electronic","value":"9783642114472"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-11447-2_7","type":"book-chapter","created":{"date-parts":[[2010,1,8]],"date-time":"2010-01-08T14:47:12Z","timestamp":1262962032000},"page":"93-110","source":"Crossref","is-referenced-by-count":4,"title":["A Systematic Verification Approach for Mondex Electronic Purses Using ASMs"],"prefix":"10.1007","author":[{"given":"Gerhard","family":"Schellhorn","sequence":"first","affiliation":[]},{"given":"Holger","family":"Grandy","sequence":"additional","affiliation":[]},{"given":"Dominik","family":"Haneberg","sequence":"additional","affiliation":[]},{"given":"Nina","family":"Moebius","sequence":"additional","affiliation":[]},{"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","unstructured":"Banach, R., Jeske, C., Poppleton, M., Stepney, S.: Retrenching the purse: The balance enquiry quandary, and generalised and (1,1) forward refinements. Fundamenta Informaticae 77 (2006)"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BFb0027289","volume-title":"ZUM\u201997: The Z Formal Specification Notation","author":"E. B\u00f6rger","year":"1997","unstructured":"B\u00f6rger, E., Mazzanti, S.: A Practical Method for Rigorously Controllable Hardware Design. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol.\u00a01212, pp. 151\u2013187. Springer, Heidelberg (1997)"},{"issue":"1\u20132","key":"7_CR3","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/s00165-003-0012-7","volume":"15","author":"E. B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E.: The ASM Refinement Method. Formal Aspects of Computing\u00a015(1\u20132), 237\u2013257 (2003)","journal-title":"Formal Aspects of Computing"},{"key":"7_CR4","series-title":"Studies in Computer Science and Artificial Intelligence","first-page":"20","volume-title":"Logic Programming: Formal Methods and Practical Applications","author":"E. B\u00f6rger","year":"1995","unstructured":"B\u00f6rger, E., Rosenzweig, D.: The WAM\u2014definition and compiler correctness. In: Beierle, C., Pl\u00fcmer, L. (eds.) Logic Programming: Formal Methods and Practical Applications. Studies in Computer Science and Artificial Intelligence, vol.\u00a011, pp. 20\u201390. North-Holland, Amsterdam (1995)"},{"key":"7_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-18216-7","volume-title":"Abstract State Machines\u2014A Method for High-Level System Design and Analysis","author":"E. B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E., St\u00e4rk, R.F.: Abstract State Machines\u2014A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)"},{"key":"7_CR6","unstructured":"Banach, R., Schellhorn, G.: On the refinement of atomic actions. In: Prooceedings of the REFINE Workshop at IFM 2007, Oxford (2007) (to appear in ENTCS)"},{"key":"7_CR7","unstructured":"Cooper, D., Stepney, S., Woodcock, J.: Derivation of Z Refinement Proof Rules: forwards and backwards rules incorporating input\/output refinement. Technical Report YCS-2002-347, University of York (2002), http:\/\/www-users.cs.york.ac.uk\/~susan\/bib\/ss\/z\/zrules.htm"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-44880-2_10","volume-title":"ZB 2003: Formal Specification and Development in Z and B","author":"J. Derrick","year":"2003","unstructured":"Derrick, J., Wehrheim, H.: Using Coupled Simulations in Non-atomic Refinement. In: Bert, D., Bowen, J.P., King, S. (eds.) ZB 2003. LNCS, vol.\u00a02651, pp. 127\u2013147. Springer, Heidelberg (2003)"},{"key":"7_CR9","first-page":"9","volume-title":"Specification and Validation Methods","author":"Y. Gurevich","year":"1995","unstructured":"Gurevich, Y.: Evolving algebras 1993: Lipari guide. In: B\u00f6rger, E. (ed.) Specification and Validation Methods, pp. 9\u201336. Oxford University Press, Oxford (1995)"},{"key":"7_CR10","unstructured":"Haneberg, D., Grandy, H., Reif, W., Schellhorn, G.: Verifying Smart Card Applications: An ASM Approach. Technical Report 2006-08, Universit\u00e4t Augsburg (2006)"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-540-73210-5_17","volume-title":"Integrated Formal Methods","author":"D. Haneberg","year":"2007","unstructured":"Haneberg, D., Grandy, H., Reif, W., Schellhorn, G.: Verifying Smart Card Applications: An ASM Approach. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol.\u00a04591, pp. 313\u2013332. Springer, Heidelberg (2007)"},{"key":"7_CR12","unstructured":"Haxthausen, A.E., George, C., Sch\u00fctz, M.: Specification and Proof of the Mondex Electronic Purse. In: Reed, M., Xin, C., Liu, Z. (eds.) Proceedings of 1st Asian Working Conference on Verified Software, AWCVS 2006, UNU-IIST Reports 348, Macau (November 2006)"},{"key":"7_CR13","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D. Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Haneberg, D., Schellhorn, G., Grandy, H., Reif, W.: Verification of Mondex Electronic Purses with KIV: From Transactions to a Security Protocol. Formal Aspects of Computing (2007) (to appear, older version available as Techn. Report 2006-32 at [KIV])","DOI":"10.1007\/s00165-007-0057-0"},{"volume-title":"Formal Aspects of Computing","year":"2007","key":"7_CR15","unstructured":"Jones, C., Woodcock, J. (eds.): Formal Aspects of Computing. Springer, Heidelberg (2007) (to appear)"},{"key":"7_CR16","unstructured":"Web presentation of the mondex case study in KIV, http:\/\/www.informatik.uni-augsburg.de\/swt\/projects\/mondex.html"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Ramananadro, T., Jackson, D.: Mondex, an electronic purse: specification and refinement checks with the alloy model-finding method (2006), http:\/\/www.eleves.ens.fr\/home\/ramanana\/work\/mondex\/","DOI":"10.1007\/s00165-007-0058-z"},{"key":"7_CR18","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1007\/978-94-017-0435-9_1","volume-title":"Automated Deduction\u2014A Basis for Applications, volume II: Systems and Implementation Techniques: Interactive Theorem Proving","author":"W. Reif","year":"1998","unstructured":"Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction\u2014A Basis for Applications, volume II: Systems and Implementation Techniques: Interactive Theorem Proving, ch.\u00a01, pp. 13\u201339. Kluwer Academic Publishers, Dordrecht (1998)"},{"key":"7_CR19","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/978-94-017-0437-3_7","volume-title":"Automated Deduction\u2014A Basis for Applications","author":"G. Schellhorn","year":"1998","unstructured":"Schellhorn, G., Ahrendt, W.: The WAM Case Study: Verifying Compiler Correctness for Prolog with KIV. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction\u2014A Basis for Applications, pp. 165\u2013194. Kluwer Academic Publishers, Dordrecht (1998)"},{"issue":"11","key":"7_CR20","first-page":"952","volume":"7","author":"G. Schellhorn","year":"2001","unstructured":"Schellhorn, G.: Verification of ASM Refinements Using Generalized Forward Simulation. Journal of Universal Computer Science (J.UCS)\u00a07(11), 952\u2013979 (2001), http:\/\/www.jucs.org","journal-title":"Journal of Universal Computer Science (J.UCS)"},{"issue":"2-3","key":"7_CR21","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1016\/j.tcs.2004.11.013","volume":"336","author":"G. Schellhorn","year":"2005","unstructured":"Schellhorn, G.: ASM Refinement and Generalizations of Forward Simulation in Data Refinement: A Comparison. Journal of Theoretical Computer Science\u00a0336(2-3), 403\u2013435 (2005)","journal-title":"Journal of Theoretical Computer Science"},{"key":"7_CR22","unstructured":"Stepney, S., Cooper, D., Woodcock, J.: AN ELECTRONIC PURSE Specification, Refinement, and Proof. Technical monograph PRG-126, Oxford University Computing Laboratory (July 2000), http:\/\/www-users.cs.york.ac.uk\/~susan\/bib\/ss\/z\/monog.htm"},{"key":"7_CR23","unstructured":"Schellhorn, G., Grandy, H., Haneberg, D., Moebius, N., Reif, W.: A systematic verification Approach for Mondex Electronic Purses using ASMs. Technical Report 2006-27, Universit\u00e4t Augsburg (2006), http:\/\/www.informatik.uni-augsburg.de\/lehrstuehle\/swt\/se\/publications\/"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/11813040_2","volume-title":"FM 2006: Formal Methods","author":"G. Schellhorn","year":"2006","unstructured":"Schellhorn, G., Grandy, H., Haneberg, D., Reif, W.: Mondex Challenge: Machine Checked Proofs for an Electronic Purse. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 16\u201331. Springer, Heidelberg (2006)"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Schellhorn, G., Grandy, H., Haneberg, D., Reif, W.: The Mondex Challenge: Machine Checked Proofs for an Electronic Purse. Technical Report 2006-2, Universit\u00e4t Augsburg (2006)","DOI":"10.1007\/11813040_2"},{"key":"7_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/11921240_2","volume-title":"Theoretical Aspects of Computing - ICTAC 2006","author":"J. Woodcock","year":"2006","unstructured":"Woodcock, J., Freitas, L.: Z\/eves and the mondex electronic purse. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol.\u00a04281, pp. 14\u201334. Springer, Heidelberg (2006)"},{"issue":"10","key":"7_CR27","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1109\/MC.2006.340","volume":"39","author":"J. Woodcock","year":"2006","unstructured":"Woodcock, J.: First steps in the verified software grand challenge. IEEE Computer\u00a039(10), 57\u201364 (2006)","journal-title":"IEEE Computer"}],"container-title":["Lecture Notes in Computer Science","Rigorous Methods for Software Construction and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11447-2_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,20]],"date-time":"2021-10-20T01:44:28Z","timestamp":1634694268000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11447-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642114465","9783642114472"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11447-2_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}