The ocfjpcsc library provides an OCF driver for PCSC compliant smart card readers. The library is based on JPCSC Java API, which is required to run ocfjpcsc. ocfjpcsc provides the same functionality as OCF To PC/SC Shim, but probably provides more stable and simpler setup for Linux - it relies on the native layer in JPCSC.
You can download the current version of ocfjpcsc here.
These JML specifications can be used to check JML annotated
Java Card 2.2.1 applets with
For more information see
NOTES file in the distribution.
You can download the current version of the Java Card API 2.2.1 specs here (a zip file here). Note: this should be still considered work in progress. If you find mistakes, bugs, ommisions, or things that you don't like, write me an e-mail.
Here you can find Java Card API 2.2.1 specifications and reference implementation for the KeY System. So far the specs are only Dynamic Logic ones. As soon as the KeY JML front-end stabilises I will make an effort to include JML specs too. There are two versions of the API available:
Together with Erik we specified and annotated in JML the Mobius Demontrator Case Study to prove so-called midlet navigation property. The case study and JML annotations are described in this technical report and this LNCS paper, the full code can be downloaded here. To verify it you will need a recent version of ESC/Java2 running on a SUN/Oracle JDK 1.4.
This case study is also published at the Verify This repository of the COST Action IC0701.
Some long time ago I also
wrote Java Card Tools
Borland Together Control Center CASE tool.
Unfortunately, it is out of date (as is Together CC) and it is not maintained anymore.