Open Access
Open access
Electronic Notes in Theoretical Computer Science, volume 240, pages 61-78

Specification and Runtime Verification of Java Card Programs

U. Costa 1
Anamaria Martins Moreira 1
Martin A. Musicante 1
Plácido A. Souza Neto 2
2
 
Centro Federal de Educação Tecnológica do Rio Grande do Norte Caixa Postal 1559 – 59.015-000 – Natal – RN - Brazil
Publication typeJournal Article
Publication date2009-07-01
Q3
SJR0.221
CiteScore
Impact factor
ISSN15710661
Theoretical Computer Science
General Computer Science
Abstract
Java Card is a version of Java developed to run on devices with severe storage and processing restrictions. The applets that run on these devices are frequently intended for use in critical, highly distributed, mobile conditions. They are required to be portable and safe. Often, the requirements of the application impose the use of dynamic, on-card verifications, but most of the research developed to improve safety of Java Card applets concentrates on static verification methods. This work presents a runtime verification approach based on Design by Contract to improve the safety of Java Card applications. To this end, we propose JCML (Java Card Modeling Language) a specification language derived from JML (Java Modeling Language) and its implementation: a compiler that generates runtime verification code. We also present some experiments and quality indicators.
Found 
Found 

Top-30

Journals

1
Computers, Materials and Continua
1 publication, 33.33%
Science of Computer Programming
1 publication, 33.33%
1

Publishers

1
Tech Science Press
1 publication, 33.33%
Elsevier
1 publication, 33.33%
Institute of Electrical and Electronics Engineers (IEEE)
1 publication, 33.33%
1
  • We do not take into account publications without a DOI.
  • Statistics recalculated only for publications connected to researchers, organizations and labs registered on the platform.
  • Statistics recalculated weekly.

Are you a researcher?

Create a profile to get free access to personal recommendations for colleagues and new articles.
Metrics
Share
Cite this
GOST |
Cite this
GOST Copy
Costa U. et al. Specification and Runtime Verification of Java Card Programs // Electronic Notes in Theoretical Computer Science. 2009. Vol. 240. pp. 61-78.
GOST all authors (up to 50) Copy
Costa U., Moreira A. M., Musicante M. A., Neto P. A. S. Specification and Runtime Verification of Java Card Programs // Electronic Notes in Theoretical Computer Science. 2009. Vol. 240. pp. 61-78.
RIS |
Cite this
RIS Copy
TY - JOUR
DO - 10.1016/j.entcs.2009.05.045
UR - https://doi.org/10.1016/j.entcs.2009.05.045
TI - Specification and Runtime Verification of Java Card Programs
T2 - Electronic Notes in Theoretical Computer Science
AU - Costa, U.
AU - Moreira, Anamaria Martins
AU - Musicante, Martin A.
AU - Neto, Plácido A. Souza
PY - 2009
DA - 2009/07/01
PB - Elsevier
SP - 61-78
VL - 240
SN - 1571-0661
ER -
BibTex
Cite this
BibTex (up to 50 authors) Copy
@article{2009_Costa,
author = {U. Costa and Anamaria Martins Moreira and Martin A. Musicante and Plácido A. Souza Neto},
title = {Specification and Runtime Verification of Java Card Programs},
journal = {Electronic Notes in Theoretical Computer Science},
year = {2009},
volume = {240},
publisher = {Elsevier},
month = {jul},
url = {https://doi.org/10.1016/j.entcs.2009.05.045},
pages = {61--78},
doi = {10.1016/j.entcs.2009.05.045}
}
Found error?