The LIME Interface Test Bench is a collection of tools that allow to compile programs in a way such that they monitor interface specifications at runtime in Java and C programs. Specifications can be made using the LIME specification language. Another part of the LIME Interface Test Bench is the LIME Concolic Testing tool (LCT), which uses a combination of concrete and symbolic execution to explore large number of control flow paths in a program or parts of a program.
The Java Card technology allows to use a limited subset of Java to develop applets that run on Smart Cards. These applets communicate with an off-card application using a simple packet-based protocol.
This report describes a case study, in which the LIME Interface Test Bench was used to test a Java Card applet. The case study uses the "logical channels demo" applet, which is part of the Java Card Development Kit [1]. Ten different specifications were added to this applet. In order to use the applet in a realistic environment, an off-card application for the applet was developed. This off-card application was tested using LCT.