Application of the B method towards the automation of Java Card component development ∗

This paper presents 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 does not need to take into account the specific aspects of the Java Card platform (in particular, communication between the card acceptance device and the smart card itself). A sequence of preestablished refinements is then applied to the original specification to yield an implementation-level B description of the component, which can then be used to synthesize Java Card code. An interesting side-effect of this approach is that the specification may be reused with any other platform of implementation. 1