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 条

[31] Verification of Java programs in Coq
Department of Computer Science, Royal Holloway University of London, Surrey, United Kingdom
Comput. Sci. Electron. Eng. Conf., CEEC,
[32] Java']JavaSplit: A runtime for execution of monolithic Java']Java programs on heterogeneous collections of commodity workstations
Factor, M
Schuster, A
Shagin, K
IEEE INTERNATIONAL CONFERENCE ON CLUSTER COMPUTING, PROCEEDINGS, 2003, : 110 - 117
[33] An Overview of the Runtime Verification Tool Java PathExplorer
Klaus Havelund
Grigore Roşu
Formal Methods in System Design, 2004, 24 : 189 - 215
[34] Formalisation and verification of JAVA']JAVA CARD security properties in dynamic logic
Mostowski, W
FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS, 2005, 3442 : 357 - 371
[35] Using contour marking bytecode verification algorithm on the java']java card
Jiang, Longlong
Li, Daiping
MECHATRONICS ENGINEERING, COMPUTING AND INFORMATION TECHNOLOGY, 2014, 556-562 : 4120 - +
[36] History-Based Specification and Verification of Java']Java Collections in KeY
Hiep, Hans-Dieter A.
Bian, Jinting
De Boer, Frank S.
De Gouw, Stijn
INTEGRATED FORMAL METHODS, IFM 2020, 2020, 12546 : 199 - 217
[37] Identifying structural features of Java']Java programs by analysing the interaction of classes at runtime
Smith, Michael P.
Munro, Malcolm
3RD IEEE INTERNATIONAL WORKSHOP ON VISUALIZING SOFTWARE FOR UNDERSTANDING AND ANALYSIS, PROCEEEDINGS, 2005, : 108 - 113
[38] Formal verification of protocol properties of sequential Java']Java programs
Jin, Ying
COMPSAC 2007: THE THIRTY-FIRST ANNUAL INTERNATIONAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE, VOL I, PROCEEDINGS, 2007, : 475 - 482
[39] On-Device Control Flow Verification for Java']Java Programs
Fontaine, Arnaud
Hym, Samuel
Simplot-Ryl, Isabelle
ENGINEERING SECURE SOFTWARE AND SYSTEMS, 2011, 6542 : 43 - 57
[40] Constraint based Testing and Verification of Java']Java Bytecode Programs
Achour, Safaa
Benattou, Mohammed
2018 IEEE 5TH INTERNATIONAL CONGRESS ON INFORMATION SCIENCE AND TECHNOLOGY (IEEE CIST'18), 2018, : 64 - 69

← 1 2 3 4 5 →