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 条
  • [1] JCML: A specification language for the runtime verification of Java']Java Card programs
    da Costa, Umberto Souza
    Moreira, Anamaria Martins
    Musicante, Martin A.
    Souza Neto, Placid A.
    SCIENCE OF COMPUTER PROGRAMMING, 2012, 77 (04) : 533 - 550
  • [2] Specification and verification of encapsulation in Java']Java programs
    Roth, A
    FORMAL METHODS FOR OPEN OBJECT-BASED DISTRIBUTED SYSTEMS, PROCEEDINGS, 2005, 3535 : 195 - 210
  • [3] A dynamic Logic for the formal verification of Java']Java Card programs
    Beckert, B
    JAVA ON SMART CARDS: PROGRAMMING AND SECURITY, 2001, 2041 : 6 - 24
  • [4] Runtime verification of Java']Java programs for scenario-based specifications
    Li Xuandong
    Wang Linzhang
    Qiu Xiaokang
    Lei Bin
    Yuan Jiesong
    Zhao Jianhua
    Zheng Guoliang
    RELIABLE SOFTWARE TECHNOLOGIES - ADA - EUROPE 2006, PROCEEDINGS, 2006, 4006 : 94 - 105
  • [5] UML interaction model-driven runtime verification of Java']Java programs
    Li, X.
    Qiu, X.
    Wang, L.
    Chen, X.
    Zhou, Z.
    Yu, L.
    Zhao, J.
    IET SOFTWARE, 2011, 5 (02) : 142 - 156
  • [6] A dynamic logic for the formal verification of java card programs
    Universität Karlsruhe, Institut für Logik, Komplexität und Deduktionssysteme, Karlsruhe
    D-76128, Germany
    Lect. Notes Comput. Sci., 1600, (6-24):
  • [7] An overview of the runtime verification tool Java']Java PathExplorer
    Havelund, K
    Rosu, G
    FORMAL METHODS IN SYSTEM DESIGN, 2004, 24 (02) : 189 - 215
  • [8] Formal specification and verification of Java']Java refactorings
    Garrido, Alejandra
    Meseguer, Jose
    SIXTH IEEE INTERNATIONAL WORKSHOP ON SOURCE CODE ANALYSIS AND MANIPULATION, PROCEEDINGS, 2006, : 165 - +
  • [9] Instruction Folding Compression for Java']Java Card Runtime Environment
    Zilli, Massimiliano
    Raschke, Wolfgang
    Weiss, Reinhold
    Steger, Christian
    Loinig, Johannes
    2014 17TH EUROMICRO CONFERENCE ON DIGITAL SYSTEM DESIGN (DSD), 2014, : 228 - 235
  • [10] jMonitor: Java']Java Runtime Event Specification and Monitoring Library
    Karaorman, Murat
    Freeman, Jay
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 113 : 181 - 200
12345