JaKarTa System
JaKarTa is a toolset for specifying and reasoning about the JavaCard platform. The main ingredients of the toolset are:
  • the JaKarTa Specification Language (JSL), a front-end for producing highly readable executable specifications;
  • the JaKarTa Transformation Kit (JTK), a program to manipulate and transform JSL specifications by abstraction and refinement;
  • the JaKarTa Prover Interface (JPI), a compiler that translates JSL specifications into proof assistants;
  • the JaKarTa Automation Kit (JAK), a toolset to support reasoning about executable specifications within proof assistants.
Goal of the work is to derive certified Byte Code Verifiers by abstraction from the specification of the JavaCard Virtual Machine.

The tool takes the JavaCard Virtual Machine specification that is developed in Coq - in the context of the CertiCartes project - as input. This is a defensive virtual machine, and by abstraction it can be transformed into a byte code verifier plus an offensive virtual machine.

JSL specifications can be translated into SPIKE specifications, and into Coq and PVS specifications (via an intermediate format with case-expressions).

 
 You may find here:
  • XaNaNa: an emacs mode for JaKarTa;
  • jtags: etags for JaKarTa;
  • JaKarTadoc: a documentation tool for JaKarTa;
  • Jakref: a references table builder for JaKarTadoc
 Downloads:
  • JaKarTa: please contact the development team (here)

Translate:

French Italian German Portuguese Spanish

Copyright © Daniela Junho de Andrade, Simão Melo de Sousa, Março 2004