Generating Control Flow Graph from Java Card Byte Code

The verification process in industrial context of embedded software in smart card is considered difficult, extremely time-consuming, and costly, with very few tools and techniques available to aid in the verification process. The work proposed in this paper consist to define the main architecture of testing java card application and a specific test model which consists of reducing a given java-card application to one method which have one input and one output data which correspond with the real communication between the card and the off-card applications. The paper details the first step of testing constraint specifications which consist of modeling and generating control flow graph in inter and intra procedural level from the byte code of java-card applications.