Automata-based approach for correct Java Card-program

The paper gives an overview of the research project which considers the generation of the dependable *Java Card* code. According to the automata-based programming technology, the code is generated from a high-level application behavior description which is based on finite state machines. An extra benefit from the use of such an approach is the possibility of the formal application specification generation. The conformance of the source or byte code against its specification could be checked by different static checking and verification tools.