Model checking of multi-applet JavaCard applications

The paper describes a framework for model checking JavaCard applets on the bytecode level. >From a set of JavaCard applets we extract their method call graphs using a static analysis tool. The resulting structure is translated into a pushdown system for which the model checking problem for Linear Temporal Logic (LTL) is decidable, and for which there are efficient model checking tools available. The model checking approach of the paper is tailored to the analysis of inter applet (intra card) communications and we demonstrate its effectiveness using a prototypical example of a purse applet and a set of loyalty applets