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.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{DeharbeGM08,
author = {David D{\'{e}}harbe and
Bruno Emerson Gurgel Gomes and
Anamaria Martins Moreira},
editor = {Egon B{\"{o}}rger and
Michael J. Butler and
Jonathan P. Bowen and
Paul Boca},
title = {BSmart: {A} Tool for the Development of Java Card Applications with
the {B} Method},
booktitle = {Abstract State Machines, {B} and Z, First International Conference,
{ABZ} 2008, London, UK, September 16-18, 2008. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5238},
pages = {351--352},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-540-87603-8\_39},
doi = {10.1007/978-3-540-87603-8\_39},
timestamp = {Tue, 14 May 2019 10:00:50 +0200},
biburl = {https://dblp.org/rec/conf/asm/DeharbeGM08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}