Abstract
A smart card is a portable computer device able to store data and execute commands. Java Card [1] is a specialization of Java, providing vendor inter-operability for smart cards, and has now reached a de facto standard status in this industry. The strategic importance of this market and the requirement for a high reliability motivate the use of rigorous software development processes for smart card aware applications based on the Java Card technology. The B method [2] is a good candidate for such process, since it is a formal method with a successful record to address industrial-level software development. In [3,4], we proposed two versions of a Java Card software development method (called BSmart) based on the B method. The main feature of these methods is to abstract the particularities of smart card systems to the applications developers as much as possible. This abstract presents the current version of a tool, also called BSmart, to support the method. The tool provides the automatable steps required by the method and some guidelines and library machines that are useful during the development process. It includes B development tools (type checker, PO generator) and specific BSmart tools (refinement generator, Java Card translator, etc.). In this approach, the card services specifier only needs to apply some refinement steps to his abstract (implementation platform independent) B specification. The generation of these refinements adapts the specification to Java Card standards and introduces platform specific aspects gradually. Finally, from the concrete B refinements the Java Card code implementing the services provided by the card will be automatically generated by the tool. The tool also provides the generation of a Java API for the host-side application from the original abstract specification, encapsulating all the communication protocol details. Thus, the client application code can then be developed in a completely platform independent way. The definition of the method is in a mature stage, and our attention is now focused on the implementation of more robust versions of the BSmart tools and packaging them in a user-friendly environment. The integration of verification and animation tools is also planned for a next release of the tool.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Chen, Z.: Java Card Technology for Smart Cards: Architecture and Programmer’s Guide. Addison Wesley, Reading (2000)
Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University (1996)
Gomes, B., Moreira, A.M., Déharbe, D.: Developing Java Card applications with B. In: SBMF, pp. 63–77 (2005)
Deharbe, D., Gomes, B.G., Moreira, A.M.: Automation of Java Card component development using the B method. In: ICECCS, pp. 259–268. IEEE Comp. Soc., Los Alamitos (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Déharbe, D., Gomes, B., Moreira, A. (2008). BSmart: A Tool for the Development of Java Card Applications with the B Method. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds) Abstract State Machines, B and Z. ABZ 2008. Lecture Notes in Computer Science, vol 5238. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87603-8_39
Download citation
DOI: https://doi.org/10.1007/978-3-540-87603-8_39
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-87602-1
Online ISBN: 978-3-540-87603-8
eBook Packages: Computer ScienceComputer Science (R0)