{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:03:37Z","timestamp":1725563017332},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642148071"},{"type":"electronic","value":"9783642148088"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14808-8_15","type":"book-chapter","created":{"date-parts":[[2010,8,21]],"date-time":"2010-08-21T09:52:01Z","timestamp":1282384321000},"page":"214-229","source":"Crossref","is-referenced-by-count":2,"title":["Analyzing a Formal Specification of Mondex Using Model Checking"],"prefix":"10.1007","author":[{"given":"Reng","family":"Zeng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xudong","family":"He","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"Argote-Garcia, G., Clarke, P.J., He, X., Fu, Y., Shi, L.: A Formal Approach for Translating a SAM Architecture to PROMELA. In: SEKE, pp. 440\u2013447 (2008)"},{"issue":"1","key":"15_CR2","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/s00165-007-0061-4","volume":"20","author":"M. Butler","year":"2007","unstructured":"Butler, M., Yadav, D.: An incremental development of the Mondex system in Event-B. Form. Asp. Comput.\u00a020(1), 61\u201377 (2007)","journal-title":"Form. Asp. Comput."},{"key":"15_CR3","unstructured":"Grand Challenges in Computer Research, United Kingdom Computing Research Committee (2008), \n                    \n                      http:\/\/www.ukcrc.org.uk\/grand_challenges\/index.cfm"},{"issue":"1","key":"15_CR4","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/s00165-007-0059-y","volume":"20","author":"L. Freitas","year":"2007","unstructured":"Freitas, L., Woodcock, J.: Mechanising Mondex with Z\/Eves. Form. Asp. Comput.\u00a020(1), 117\u2013139 (2007)","journal-title":"Form. Asp. Comput."},{"key":"15_CR5","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1109\/ASE.2001.989839","volume-title":"ASE 2001: Proceedings of the 16th IEEE international conference on Automated software engineering","author":"G.C. Gannod","year":"2001","unstructured":"Gannod, G.C., Gupta, S.: An Automated Tool for Analyzing Petri Nets Using SPIN. In: ASE 2001: Proceedings of the 16th IEEE international conference on Automated software engineering, Washington, DC, USA, 2001, p. 404. IEEE Computer Society, Los Alamitos (2001)"},{"issue":"1","key":"15_CR6","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/s00165-007-0054-3","volume":"20","author":"C. George","year":"2007","unstructured":"George, C., Haxthausen, A.E.: Specification, proof, and model checking of the Mondex electronic purse using RAISE. Form. Asp. Comput.\u00a020(1), 101\u2013116 (2007)","journal-title":"Form. Asp. Comput."},{"issue":"1","key":"15_CR7","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1093\/comjnl\/45.1.111","volume":"45","author":"X. He","year":"2002","unstructured":"He, X., Deng, Y.: A Framework for Developing and Analyzing Software Architecture Specifications in SAM. The Computer Journal\u00a045(1), 111\u2013128 (2002)","journal-title":"The Computer Journal"},{"key":"15_CR8","volume-title":"The Electrical Engineering Handbook","author":"X. He","year":"2005","unstructured":"He, X., Murata, T.: High-Level Petri Nets - Extensions, Analysis, and Applications. In: The Electrical Engineering Handbook, Elsevier Academic Press, Amsterdam (2005)"},{"key":"15_CR9","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"G. Holzmann","year":"2003","unstructured":"Holzmann, G.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley Professional, Reading (2003)"},{"issue":"1","key":"15_CR10","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/s00165-007-0057-0","volume":"20","author":"D. Haneberg","year":"2007","unstructured":"Haneberg, D., Schellhorn, G., Grandy, H., Reif, W.: Verification of Mondex electronic purses with KIV: from transactions to a security protocol. Form. Asp. Comput.\u00a020(1), 41\u201359 (2007)","journal-title":"Form. Asp. Comput."},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/3-540-47884-1_9","volume-title":"Integrated Formal Methods","author":"S. Katz","year":"2002","unstructured":"Katz, S., Grumberg, O.: A Framework for Translating Models and Specifications. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol.\u00a02335, pp. 145\u2013164. Springer, Heidelberg (2002)"},{"issue":"1","key":"15_CR12","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s00165-007-0058-z","volume":"20","author":"T. Ramananandro","year":"2007","unstructured":"Ramananandro, T.: Mondex, an electronic purse: specification and refinement checks with the Alloy model-finding method. Form. Asp. Comput.\u00a020(1), 21\u201339 (2007)","journal-title":"Form. Asp. Comput."},{"key":"15_CR13","unstructured":"Stepney, S., Cooper, D., Woodcock, J.: An Electronic Purse: Specification, Refinement, and Proof. Technical monograph PRG-126, Oxford University Computing Laboratory (July 2000)"},{"key":"15_CR14","unstructured":"Verified Software Repository (2007), \n                    \n                      http:\/\/vsr.sourceforge.net"},{"issue":"10","key":"15_CR15","doi-asserted-by":"publisher","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. Computer\u00a039(10), 57\u201364 (2006)","journal-title":"Computer"},{"issue":"1","key":"15_CR16","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s00165-007-0060-5","volume":"20","author":"J. Woodcock","year":"2007","unstructured":"Woodcock, J., Stepney, S., Cooper, D., Clark, J., Jacob, J.: The certification of the Mondex electronic purse to ITSEC Level E6. Form. Asp. Comput.\u00a020(1), 5\u201319 (2007)","journal-title":"Form. Asp. Comput."},{"key":"15_CR17","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1109\/SOSE.2008.25","volume-title":"SOSE 2008: Proceedings of the 2008 IEEE International Symposium on Service-Oriented System Engineering","author":"R. Zeng","year":"2008","unstructured":"Zeng, R., Liu, J., He, X.: A Formal Specification of Mondex Using SAM. In: SOSE 2008: Proceedings of the 2008 IEEE International Symposium on Service-Oriented System Engineering, Jhongli, Taiwan, pp. 97\u2013102. IEEE Computer Society, Los Alamitos (2008)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2010"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14808-8_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T21:20:32Z","timestamp":1558300832000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14808-8_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642148071","9783642148088"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14808-8_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}