{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,14]],"date-time":"2023-01-14T22:48:09Z","timestamp":1673736489589},"reference-count":32,"publisher":"International Academy Publishing (IAP)","issue":"9","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["JSW"],"DOI":"10.4304\/jsw.7.9.1941-1949","type":"journal-article","created":{"date-parts":[[2012,10,4]],"date-time":"2012-10-04T09:49:29Z","timestamp":1349344169000},"source":"Crossref","is-referenced-by-count":5,"title":["Model Checking and Verification of the Internet Payment System with SPIN"],"prefix":"10.17706","volume":"7","author":[{"given":"Wei","family":"Zhang","sequence":"first","affiliation":[]},{"given":"Wen-ke","family":"Ma","sequence":"additional","affiliation":[]},{"given":"Hui-ling","family":"Shi","sequence":"additional","affiliation":[]},{"given":"Fu-qiang","family":"Zhu","sequence":"additional","affiliation":[]}],"member":"7163","published-online":{"date-parts":[[2012,9,1]]},"reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2008.01.005"},{"key":"ref2","doi-asserted-by":"crossref","first-page":"609","DOI":"10.1016\/j.comcom.2004.08.006","article-title":"Model checking active networks with SPIN","volume":"28","author":"Gallardo","year":"2005","unstructured":"[2] M. M. Gallardo, J. Martinez and P. Merino, \"Model checking active networks with SPIN,\" Computer Communications, Elsevier, vol.28, pp. 609\u2013622, 2005.","journal-title":"Computer Communications Elsevier"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"ref4","volume-title":"E Clarke O Grumberg and D Peled Model Checking","year":"2000","unstructured":"[4] E. Clarke, O. Grumberg and D. Peled, Model Checking, MIT Press, Cambridge, 2000."},{"key":"ref5","volume-title":"Design and Validation of Comp Protocols","author":"Holzmann","year":"1991","unstructured":"[5] G.J. Holzmann, Design and Validation of Comp. Protocols, Prentice-Hall, Englewood Cliffs, NJ, 1991"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"issue":"4","key":"ref7","first-page":"1","article-title":"Formal methods: State of the art and future directions","volume":"28","author":"Clark","year":"1996","unstructured":"[8] E. M. Clark and J. M. Wing, \"Formal methods: State of the art and future directions,\" ACM Computing Surveys, Vol. 28(4), pp. 1\u201318, 1996.","journal-title":"ACM Comput Surv","ISSN":"http:\/\/id.crossref.org\/issn\/0360-0300","issn-type":"print"},{"key":"ref8","volume-title":"The SPIN Model Checker Primer and Reference Manual","author":"Holzmann","year":"2004","unstructured":"[12] G. J. Holzmann, The SPIN Model Checker: Primer and Reference Manual, Addison Wesley, 2004."},{"issue":"No. 4","key":"ref9","first-page":"179","article-title":"Model Checking Bidding Behaviors in Internet Concurrent Auctions","volume":"22","author":"Xu","year":"2007","unstructured":"[13] H. Xu and Y-T. Cheng, \"Model Checking Bidding Behaviors in Internet Concurrent Auctions,\" International Journal of Computer Systems Science & Engineering (IJCSSE), Vol. 22, No. 4, pp. 179\u2013191, July 2007.","journal-title":"International Journal of Computer Systems Science & Engineering"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008615614281"},{"key":"ref12","volume-title":"An Introduction to Electronic Commerce","author":"Pombortsis","year":"2002","unstructured":"[18] A. Pombortsis and A. Tsoulfas, An Introduction to Electronic Commerce, Tziolas Publishers, 2002."},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/2.612244"},{"key":"ref14","first-page":"146","article-title":"Model checking electronic commerce protocols","volume-title":"Proceedings of the Second USENIX Work-shop in Electronic","author":"Heintze","year":"1996","unstructured":"[22] N. Heintze, J. Tygar, J. Wing, et al. \"Model checking electronic commerce protocols,\" Proceedings of the Second USENIX Work-shop in Electronic Commerce, Oakland, CA, USENIX Association, California, pp. 146\u2013164, 1996."},{"key":"ref15","doi-asserted-by":"crossref","DOI":"10.1109\/WECWIS.2000.853873","article-title":"Failure analysis of an e-commerce protocol using model checking","volume-title":"Proceedings of the Second International Work-shop on Advanced Issues of e-Commerce and Web-based Information Systems","author":"Ray","year":"2000","unstructured":"[24] I. Ray, \"Failure analysis of an e-commerce protocol using model checking,\" Proceedings of the Second International Work-shop on Advanced Issues of e-Commerce and Web-based Information Systems, Milpitas, CA, 2000."},{"key":"ref16","article-title":"Netbill security and transaction protocol","volume-title":"Proceedings of the First USENIX Workshop in Electronic Commerce","author":"Cox","year":"1995","unstructured":"[26] B. Cox, J. Tygar and M. Sirbu, \"Netbill security and transaction protocol,\" Proceedings of the First USENIX Workshop in Electronic Commerce, July 1995."},{"issue":"4","key":"ref17","first-page":"479","article-title":"Internet Payment System: A new payment system for internet transactions","volume":"13","author":"Duric","year":"2007","unstructured":"[28] Z. Duric, O. Maric and D. Gasevic, \"Internet Payment System: A new payment system for internet transactions,\" Journal of Universal Computer Science, vol. 13(4), pp.479-503, 2007.","journal-title":"Journal of Universal Computer Science"},{"key":"ref18","first-page":"214","volume-title":"Analyzing a formal specification of mondex using model checking","volume":"6255","author":"Zeng","year":"2010","unstructured":"[29] R. Zeng and X. He, \"Analyzing a formal specification of mondex using model checking,\" Lecture Notes in Computer Science, Springer-Verlag, Berlin Heidelberg, vol.6255, pp. 214-229, 2010."},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1016\/j.knosys.2008.11.006"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.08.069"},{"key":"ref20","doi-asserted-by":"crossref","unstructured":"[7] On-the-fly LTL model checking with SPIN. http:\/\/spinroot.com\/spin\/whatispin.html","DOI":"10.1016\/j.entcs.2004.08.069"},{"key":"ref20","doi-asserted-by":"crossref","unstructured":"[9] A. Cimatti, E. M. Clarke, E. Giunchiglia, et al. \"NuSMV2: An OpenSource Tool for Symbolic Model Checking,\" Proceeding of International Conference on Computer-Aided Verification (CAV2002), Copenhagen, Denmark, July 2002.","DOI":"10.1016\/j.entcs.2004.08.069"},{"key":"ref20","doi-asserted-by":"crossref","unstructured":"[10] K. Havelund. \"Java PathFinder: A Translator from Java to PROMELA,\" Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, Springer-Verlag, pp. 152, 1999.","DOI":"10.1016\/j.entcs.2004.08.069"},{"key":"ref20","doi-asserted-by":"crossref","unstructured":"[11] M. Makela, \"Maria: Modular Reachability Analyser for Algebraic System,\" Application and Theory of Petri Nets 2002, 23rd International Conference, ICATPN 2002, Vol. 2360, pp. 434\u2013444, June 2002.","DOI":"10.1016\/j.entcs.2004.08.069"},{"key":"ref20","doi-asserted-by":"crossref","unstructured":"[16] R. Shaikh and S. Devane, \"Formal verification of payment protocol using AVISPA,\" International Journal for Infonomics, Vol.3, Issue 3, September 2010.","DOI":"10.1016\/j.entcs.2004.08.069"},{"key":"ref20","doi-asserted-by":"crossref","unstructured":"[17] H.M. Deitel, P.J. Deitel and T.R. Nieto, e-Business & e-Commerce: How to Program, Prentice Hall, 2001.","DOI":"10.1016\/j.entcs.2004.08.069"},{"key":"ref20","doi-asserted-by":"crossref","unstructured":"[19] L. Ferreira and C. Dahab, \"A scheme for analyzing electronic payment systems,\" Proceedings of the 14th Annual Computer Security Applications Conference, IEEE Computer Society, pp.137\u2013146, 1998.","DOI":"10.1016\/j.entcs.2004.08.069"},{"key":"ref20","doi-asserted-by":"crossref","unstructured":"[21] H. Schuldt, A. Popovici and H.J. Schek, \"Automatic generation of reliable e-commerce payment processes,\" Proceedings of the First International Conference on Web Information Systems Engineering (WISE00), IEEE Computer Society, vol. 1, pp. 434\u2013441, 2000.","DOI":"10.1016\/j.entcs.2004.08.069"},{"key":"ref20","doi-asserted-by":"crossref","unstructured":"[23] B. Pfitzmann and M. Waidner, \"Properties of payment systems \u2013 General definition sketch and classification,\" Research Report RZ 2823(#90126), IBM Research Division, May 1996.","DOI":"10.1016\/j.entcs.2004.08.069"},{"key":"ref20","doi-asserted-by":"crossref","unstructured":"[25] D. Chaum, A. Fiat and M. Naor, \"Untraceable electronic cash,\" Advances in Cryptology, CRYPTO '88 Proceedings, 1990.","DOI":"10.1016\/j.entcs.2004.08.069"},{"key":"ref20","doi-asserted-by":"crossref","unstructured":"[27] G. Lowe, \"Breaking and fixing the needham-schroeder publickey protocol using FDR,\" Tools and Algorithms for the Construction and Analysis of Systems: Second International Work-shop, TACAS, March 1996.","DOI":"10.1016\/j.entcs.2004.08.069"},{"key":"ref20","doi-asserted-by":"crossref","unstructured":"[30] H. Cao, S. Ying and D. Du, \"Towards model-based verification of BPEL with model checking,\" Proceedings of the sixth IEEE international conference on computer and information technology (CIT06), IEEE, 2006.","DOI":"10.1016\/j.entcs.2004.08.069"}],"container-title":["Journal of Software"],"original-title":[],"deposited":{"date-parts":[[2017,6,21]],"date-time":"2017-06-21T00:59:42Z","timestamp":1498006782000},"score":1,"resource":{"primary":{"URL":"http:\/\/ojs.academypublisher.com\/index.php\/jsw\/article\/view\/6552"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,9,1]]},"references-count":32,"journal-issue":{"issue":"9","published-online":{"date-parts":[[2012,9,1]]}},"URL":"https:\/\/doi.org\/10.4304\/jsw.7.9.1941-1949","relation":{},"ISSN":["1796-217X"],"issn-type":[{"value":"1796-217X","type":"print"}],"subject":[],"published":{"date-parts":[[2012,9,1]]}}}