Developing Java Card Applications with B

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 specification of the aplication logic needs not be preoccupied with the specific aspects of the Java Card platform (in particular, communication between the card acceptance 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.