Guaranteeing Correctness Properties of a Java Card Applet

The paper describes an experiment in which a framework for model checking Java byte code, combined with the application of runtime monitoring techniques through code rewriting, was used to guarantee correctness properties of a Java Card applet.

Saved in:
Bibliographic Details
Published in:Electronic notes in theoretical computer science 2005-01, Vol.113, p.217-233
Main Author: Fredlund, Lars-Åke
Format: Article
Language:English
Subjects:
code rewriting
Java byte code
Java Card
runtime monitoring
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The paper describes an experiment in which a framework for model checking Java byte code, combined with the application of runtime monitoring techniques through code rewriting, was used to guarantee correctness properties of a Java Card applet.
ISSN:1571-0661
1571-0661
DOI:10.1016/j.entcs.2004.01.033