Model checking of multi-applet javacard applications
Gennady Chugunov, Lars‐Åke Fredlund, Dilian Gurov · 2002
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 ecient 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 it using a prototypical example of a purse applet and a set of loyalty applets.