Specification and Runtime Verification of Java']Java Card Programs

被引：1

作者：

da Costa, Umberto Souza ^{[1
]}

Moreira, Anamaria Martins ^{[1
]}

Musicante, Martin A. ^{[1
]}

Souza Neto, Placido A. ^{[2
]}

机构：

[1] Univ Fed Rio Grande do Norte, DIMAp, Campus Univ, Natal, RN, Brazil

[2] Ctr Fed Educ Tecnol Rio Grande Norte, BR-1559 Natal, RN, Brazil

来源：

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2009年 / 240卷

关键词：

JML; !text type='Java']Java[!/text] Card; JCML; Compiler; Runtime Verification;

D O I：

10.1016/j.entcs.2009.05.045

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：61 / 78

页数：18

共 50 条

[21] API Conformance Verification for Java']Java Programs
Li, Xin
Hoover, H. James
Rudnicki, Piotr
FORMAL METHODS AND SOFTWARE ENGINEERING, 2010, 6447 : 188 - 203
[22] Measurement and analysis of runtime profiling data for Java']Java programs
Horgan, J
Power, J
Waldron, J
FIRST IEEE INTERNATIONAL WORKSHOP ON SOURCE CODE ANALYSIS AND MANIPULATION, PROCEEDINGS, 2001, : 122 - 130
[23] Verification of JAVA']JAVA CARD applets behavior with respect to transactions and card tears
Marche, Claude
Rousset, Nicolas
SEFM 2006: FOURTH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS, 2006, : 137 - +
[24] An eclipse plug-in for the Java']Java PathFinder runtime verification system
Arcelli, Francesca
Raibulet, Claudia
Rigo, Ivano
Ubezio, Luigi
30TH ANNUAL IEEE/NASA SOFTWARE ENGINEERING WORKSHOP, PROCEEDINGS, 2006, : 142 - +
[25] Using runtime analysis to guide model checking of Java']Java programs
Havelund, K
SPIN MODEL CHECKING AND SOFTWARE VERIFICATON, 2000, 1885 : 245 - 264
[26] Automatic verification of Java']Java programs with dynamic frames
Smans, Jan
Jacobs, Bart
Piessens, Frank
Schulte, Wolfram
FORMAL ASPECTS OF COMPUTING, 2010, 22 (3-4) : 423 - 457
[27] Runtime Exception Detection in Java']Java Programs Using Symbolic Execution
Kadar, Istvan
Hegedus, Peter
Ferene, Rudolf
ACTA CYBERNETICA, 2014, 21 (03): : 331 - 352
[28] Verification of Java']Java Programs with Interacting Analysis Plugins
Charlton, Nathaniel
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 145 : 131 - 150
[29] Implementing FISCIC card specification and developing health care application using Java']Java card
Ma, TY
Hou, TW
INTERNATIONAL SYMPOSIUM ON MULTIMEDIA SOFTWARE ENGINEERING, PROCEEDINGS, 2000, : 184 - 190
[30] Towards the automated verification of multithreaded Java']Java programs
Delzanno, G
Raskin, JF
Van Begin, L
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANAYLSIS OF SYSTEMS, PROCEEDINGS, 2002, 2280 : 173 - 187

← 1 2 3 4 5 →