Towards Verification of Well-Formed Transactions in Java Card Bytecode |
Rene Rydhof Hansen, Igor Siveroni
|
| Abstract | Using 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. |
| Keywords | java card, static analysis, well-formed transactions, flow logic |
| Type | Conference paper [With referee] |
| Conference | Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE) |
| Editors | Fausto Spoto |
| Year | 2005 |
| Publisher | Elsevier |
| Series | Electronic Notes in Computer Science |
| Note | To appear |
| Electronic version(s) | [pdf] |
| BibTeX data | [bibtex] |
| IMM Group(s) | Computer Science & Engineering |