{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T14:48:16Z","timestamp":1725547696705},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642118104"},{"type":"electronic","value":"9783642118111"}],"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-11811-1_16","type":"book-chapter","created":{"date-parts":[[2010,2,19]],"date-time":"2010-02-19T06:57:22Z","timestamp":1266562642000},"page":"203-216","source":"Crossref","is-referenced-by-count":4,"title":["Applying the B Method for the Rigorous Development of Smart Card Applications"],"prefix":"10.1007","author":[{"given":"Bruno","family":"Gomes","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"D\u00e9harbe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anamaria","family":"Moreira","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Katia","family":"Moraes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","volume-title":"Java Card Technology for Smart Cards: Architecture and Programmer\u2019s Guide","author":"Z. Chen","year":"2000","unstructured":"Chen, Z.: Java Card Technology for Smart Cards: Architecture and Programmer\u2019s Guide. Addison Wesley, Reading (2000)"},{"key":"16_CR2","unstructured":"Gomes, B., Moreira, A.M., D\u00e9harbe, D.: Developing Java Card applications with B. In: Brazilian Symposium on Formal Methods (SBMF), pp. 63\u201377 (2005)"},{"key":"16_CR3","first-page":"259","volume-title":"ICECCS","author":"D. Deharbe","year":"2006","unstructured":"Deharbe, D., Gomes, B.G., Moreira, A.M.: Automation of Java Card component development using the B method. In: ICECCS, pp. 259\u2013268. IEEE Comp. Soc., Los Alamitos (2006)"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-540-87603-8_39","volume-title":"Abstract State Machines, B and Z","author":"D. D\u00e9harbe","year":"2008","unstructured":"D\u00e9harbe, D., Gomes, B.G., Moreira, A.M.: Bsmart: A Tool for the Development of Java Card Applications with the B Method. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol.\u00a05238, pp. 351\u2013352. Springer, Heidelberg (2008)"},{"key":"16_CR5","unstructured":"Ortiz, E.C.: An Introduction to Java Card Technology, \n                    \n                      http:\/\/java.sun.com\/javacard\/reference\/techart\/javacard1\n                    \n                    \n                   (2003)"},{"key":"16_CR6","unstructured":"PC\/SC Workgroup: PC\/SC Workgroup Web site (2009), \n                    \n                      http:\/\/www.pcscworkgroup.com"},{"key":"16_CR7","unstructured":"Global Platform: Global Platform Web site (2009), \n                    \n                      http:\/\/www.globalplatform.org"},{"key":"16_CR8","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"J.R. Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge U. Press, Cambridge (1996)"},{"key":"16_CR9","unstructured":"D\u00e9harbe, D., Gomes, B.G., Moreira, A.M.: Refining Interfaces: The Case of the B Method. Technical report, Fed. Univ. of Rio Grande do Norte (2009) (to appear)"},{"key":"16_CR10","unstructured":"Voisinet, J.C.: JBtools: an experimental platform for the formal B method. In: Principles and Practice of Programming, Maynooth, NUI, pp. 137\u2013139 (2002)"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/3-540-45418-7_14","volume-title":"Smart Card Programming and Security","author":"H. Meijer","year":"2001","unstructured":"Meijer, H., Poll, E.: Towards a Full Formal Specification of the Java Card API. In: Attali, S., Jensen, T. (eds.) E-smart 2001. LNCS, vol.\u00a02140, pp. 165\u2013178. Springer, Heidelberg (2001)"},{"key":"16_CR12","unstructured":"Larsson, D.: OCL Specifications for the Java Card API. Master\u2019s thesis, School of Computer Science and Engineering, G\u00f6teborg University (2003)"},{"key":"16_CR13","first-page":"15","volume-title":"ICFEM 2000","author":"A. Requet","year":"2000","unstructured":"Requet, A., Bossu, G.: Embedded formally proved code in a smart card: Converting B to C. In: ICFEM 2000, York, UK, p. 15. IEEE Computer Society, Los Alamitos (2000)"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1007\/978-3-540-45236-2_7","volume-title":"FME 2003: Formal Methods","author":"D. Bert","year":"2003","unstructured":"Bert, D., et al.: Adaptable translator of B specifications to embedded C programs. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 94\u2013113. Springer, Heidelberg (2003)"},{"key":"16_CR15","unstructured":"Edmunds, A., Butler, M.: Code Generation for Event-B with Intermediate Specification. In: Rodin User and Developers Workshop (2009), \n                    \n                      http:\/\/wiki.event-b.org\/index.php\/Rodin_Workshop_2009"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"306","DOI":"10.1007\/978-3-540-39893-6_18","volume-title":"Formal Methods and Software Engineering","author":"B. Tatibouet","year":"2003","unstructured":"Tatibouet, B., Requet, A., Voisinet, J., Hammad, A.: Java Card Code Generation from B Specifications. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol.\u00a02885, pp. 306\u2013318. Springer, Heidelberg (2003)"},{"key":"16_CR17","unstructured":"Costa, U., Moreira, A., Musicante, M., Neto, P.: Specification and Runtime Verification of Java Card Programs. In: Brazilian Symp. on Formal Methods (2008)"},{"key":"16_CR18","unstructured":"Cordy, J.: The TXL Programming Language (2009), \n                    \n                      http:\/\/www.meta-environment.org"},{"key":"16_CR19","unstructured":"Meta-Environment.org: The ASF+SDF Meta-Environment (2009), \n                    \n                      http:\/\/www.txl.ca\/index.html"},{"issue":"1","key":"16_CR20","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. Formal Aspects of Computing\u00a020(1), 61\u201377 (2007)","journal-title":"Formal Aspects of Computing"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B and Z"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11811-1_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:43:42Z","timestamp":1558273422000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11811-1_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642118104","9783642118111"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11811-1_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}