Formal Engineering Methods, International Conference on (2000)
Sept. 4, 2000 to Sept. 7, 2000
Antoine Requet , Gemplus Research Laboratory
Gaëlle Bossu , LIFC
Smart cards are small-embedded devices with strong security requirements. To fulfill those requirements, formal methods appear as promising techniques. The B method has already been used to model smart card components. However, smart cards have also very strong programming constraints, for both memory usage and computing power. Currently the code generated from a B specification does not meet those constraints. This paper presents some classical optimisation techniques that are well suited for B specifications, and that need to be included within a code generator to embed this generated code.
G. Bossu and A. Requet, "Embedding Formally Proved Code in a Smart Card: Converting B to C," Formal Engineering Methods, International Conference on(ICFEM), York, England, 2000, pp. 15.