Towards Verification of Well-Formed Transactions in Java Card Bytecode

Rene Rydhof Hansen, Igor Siveroni

AbstractUsing transactions in Java Card bytecode programs can be rather tricky
and requires special attention from the programmer in order to work
around some of the limitations imposed and to avoid introducing
serious run-time errors due to inappropriate use of transactions.

In this paper we present a novel analysis that combines control and
data flow analysis with an analysis that tracks active transactions in
a Java Card bytecode program. We formally prove the correctness of the
analysis and show how it can be used to solve the above problem of
guaranteeing that transactions in a Java Card bytecode program are
well-formed and thus do not give rise to run-time errors.
Keywordsjava card, static analysis, well-formed transactions, flow logic
TypeConference paper [With referee]
ConferenceWorkshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE)
EditorsFausto Spoto
Year2005
PublisherElsevier
SeriesElectronic Notes in Computer Science
NoteTo appear
Electronic version(s)[pdf]
BibTeX data [bibtex]
IMM Group(s)Computer Science & Engineering