Developing Java Card Applications with B

Abstract. This work proposes a methodology for the rigorous development of Java Card smart card applications, using the B Method. Its main feature is to abstract the particularities of Java Card and smart card aware applications from the specifier as much as possible. In the proposed approach, the specifi-cation of the aplication logic needs not be preoccupied with the specific aspects of the Java Card platform (in particular, communication between the card ac-ceptance device and the smart card itself). Platform-specific code can then be automatically generated during the refinement and code generation process. An interesting side-effect of this approach is that the specification may be reused with any other platform of implementation. 1