DEVELOPMENT OF CORECT JAVA CARD-APPLICATION WITH AUTOMATA-BASED APPROACH

Клебанов Андрей Александрович, Shalyto Anatoly A.

2008 , VOLUME 08, NUMBER 8 ( April )

ISSN 2226-1494 (print), ISSN 2500-0373 (online)

Publications

Editor-in-Chief

Nikiforov
Vladimir O.
D.Sc., Prof.

Partners

DEVELOPMENT OF CORECT JAVA CARD-APPLICATION WITH AUTOMATA-BASED APPROACH

Клебанов А.А., A. A. Shalyto

Read the full article

Abstract

In this paper describes the results of studies aimed at establishing the correct Java Card-code. In doing so, the code is generated from the high level description of automata-based programming. An additional advantage of this approach is the ability to generate a formal specification of the application. Compliance with the source or byte-code specifications can be verified by various verifiers or tools for dynamic and static testing.

Keywords: program verification, Java Card, automata-based programming

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License