A Development and Simulation Environment for Java Card based upon a Formal Semantics

For better understanding, you should have read the presentation of this environment before going on.



A formal definition for JavaCard

  1. The Java Card syntax was specified in order to be able to parse a Java Card program. Indeed when a program is read in the Centaur system, an abstract syntax tree is built during the parsing. This tree is for structured editing or interpretation (see window below).
  2. A pretty-printer was defined to display this tree to an user in a textual manner (see the example program source code window below)
  3. We have started to specify a Formal Semantics for Java Card in order to simulate applets
Java Card Program without Pretty-Printer



The Example Program Souce Code Window

This window contains the source code used for the example program (the program is the same as the program above but displayed with a pretty-printer). The goal of this program is the simulate the behavior of the actors (JCRE, CAD, User) that interact with the applets.

Java Card Program with Pretty-Printer


Click here if you want to read the full simulation program.


The Object Interactions Window

During the interpretation of the example program, the applet developer can watch a graphical display interactions between objects and threads, their states (running, suspended...), attribute values as well as class variables.
In this figure, the Root thread is running (green oval with a blue circle around) and initializes all the actors useful to perform a transaction. The User thread and the JCRE thread are suspended (brown), the CAD thread has just been created (flashy green). The APDU object is a simple object (blue). The golden yellow ovals contain class variables.
In this figure, the Root thread (useful only for the initialization part) is dead (black color), the User thread is running, the APDUs (#5 and #3) are simple objects and the other ones are suspended threads. There is no applet on the card.
This figure shows that we can zoom an object to inspect attribute values or zoom a class to inspect class variables.
The purseFr thread is running. It has just received a select() request from the JCRE because the user wants to withdraw 100 Francs.
In this figure, the JCRE thread is running, the other threads are suspended

The APDUs Windows

APDUs exchanged between the CAD and the JCRE in order to perform a transaction are shown in the first window (for the moment, our values are not ISO 7816 compliant). This format is not easy to read, this is the reason why we provide the second window that gives which action is performed.

i





[Home]		 Please send us an email if your have any comment or request.
http://www-sop.inria.fr/oasis/javacard/environment
Since November, 17th, 1998, you are our th visitor.
Thanks for visiting!
Last Update: Tue Nov 17 19:05:30 MET 1998