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 条
  • [41] Verification of Snapshot Isolation in Transactional Memory Java']Java Programs
    Dias, Ricardo J.
    Distefano, Dino
    Seco, Joao Costa
    Lourenco, Joao M.
    ECOOP 2012 - OBJECT-ORIENTED PROGRAMMING, 2012, 7313 : 640 - 664
  • [42] A Framework for the Cryptographic Verification of Java']Java-like Programs
    Kuesters, Ralf
    Truderung, Tomasz
    Graf, Juergen
    2012 IEEE 25TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF), 2012, : 198 - 212
  • [43] Using Krakatoa for Teaching Formal Verification of Java']Java Programs
    Divason, Jose
    Romero, Ana
    FORMAL METHODS TEACHING (FMTEA 2019), 2019, 11758 : 37 - 51
  • [44] Implementation of Revocable Keyed-Verification Anonymous Credentials on Java']Java Card
    Casanova-Marques, Raul
    Dzurenda, Petr
    Hajny, Jan
    PROCEEDINGS OF THE 17TH INTERNATIONAL CONFERENCE ON AVAILABILITY, RELIABILITY AND SECURITY, ARES 2022, 2022,
  • [45] Towards Verification of Well-Formed Transactions in Java']Java Card Bytecode
    Hansen, Rene Rydhof
    Siveroni, Igor A.
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 141 (01) : 145 - 162
  • [46] Verification of Java']JavaSpaces™ parallel programs
    van de Pol, J
    Espada, MV
    THIRD INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN, PROCEEDINGS, 2003, : 196 - 205
  • [47] The KaffeOS Java']Java runtime system
    Back, G
    Hsieh, WC
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2005, 27 (04): : 583 - 630
  • [48] Advanced Runtime Adaptation for Java']Java
    Villazon, Alex
    Binder, Walter
    Ansaloni, Danilo
    Moret, Philippe
    ACM SIGPLAN NOTICES, 2010, 45 (02) : 85 - 94
  • [49] Towards a Serverless Java']Java Runtime
    Zhang, Yifei
    Gu, Tianxiao
    Zheng, Xiaolin
    Yu, Lei
    Kuai, Wei
    Li, Sanhong
    2021 36TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING ASE 2021, 2021, : 1156 - 1160
  • [50] Experiences and New Alternatives for Teaching Formal Verification of Java']Java Programs
    Romero, Ana
    Divason, Jose
    ITICSE'18: PROCEEDINGS OF THE 23RD ANNUAL ACM CONFERENCE ON INNOVATION AND TECHNOLOGY IN COMPUTER SCIENCE EDUCATION, 2018, : 383 - 383
12345