A refinement method for Java']Java programs

被引：0
|
作者：
Grandy, Holger [1 ]
Stenzel, Kurt [1 ]
Reif, Wolfgang [1 ]
机构：
[1] Univ Augsburg, Inst Informat, Lehrstuhl Softwaretech & Programmiersprachen, D-86135 Augsburg, Germany
来源：
FORMAL METHODS FOR OPEN OBJECT-BASED DISTRIBUTED SYSTEMS, PROCEEDINGS | 2007年 / 4468卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We present a refinement method for Java programs which is motivated by the challenge of verifying security protocol implementations. The method can be used for stepwise refinement of abstract specifications down to the level of code running in the real application. The approach is based on a calculus for the verification of Java programs for the concrete level and Abstract State Machines for the abstract level. In this paper we illustrate our method by the verification of a M-Commerce application for buying movie tickets using a mobile phone written in J2ME. For verification we use KIV, our interactive theorem prover [1].
引用
收藏
页码：221 / +
页数：3
相关论文
共 50 条
  • [41] Converting Physlets and Other Java']Java Programs to Java']JavaScript
    Christian, Wolfgang
    Belloni, Mario
    Hanson, Robert M.
    Mason, Bruce
    Barbato, Lyle
    PHYSICS TEACHER, 2021, 59 (04): : 278 - 281
  • [42] Proposal of a Visualizing Method of Data Transitions to Support Debugging for Java']Java Programs
    Katayama, Tetsuro
    Nakamura, Hiroto
    Kita, Yoshihiro
    Yamaba, Hisaaki
    Okazaki, Naonobu
    JOURNAL OF ROBOTICS NETWORKING AND ARTIFICIAL LIFE, 2014, 1 (02): : 111 - 115
  • [43] Proposal of a Visualizing Method of Data Transitions to Support Debugging for Java']Java Programs
    Nakamura, Hiroto
    Katayama, Tetsuro
    Kita, Yoshihiro
    Yamaba, Hisaaki
    Okazaki, Naonobu
    PROCEEDINGS OF INTERNATIONAL CONFERENCE ON ARTIFICIAL LIFE AND ROBOTICS (ICAROB 2014), 2014, : 210 - 213
  • [44] JEvTrace: refinement and variations of the evolutionary trace in JAVA']JAVA
    Joachimiak, Marcin P.
    Cohen, Fred E.
    GENOME BIOLOGY, 2002, 3 (12):
  • [45] Checking and Correcting Behaviors of Java']Java Programs at Runtime with Java']Java-MOP
    Chen, Feng
    d'Amorim, Marcelo
    Rosu, Grigore
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 144 (04) : 3 - 20
  • [46] Towards the Generation of Correct Java']Java Programs
    Philippe, Jolan
    Loulergue, Frederic
    PROCEEDINGS 2018 INTERNATIONAL CONFERENCE ON HIGH PERFORMANCE COMPUTING & SIMULATION (HPCS), 2018, : 1055 - 1056
  • [47] Data size optimizations for Java']Java programs
    Ananian, CS
    Rinard, M
    ACM SIGPLAN NOTICES, 2003, 38 (07) : 59 - 68
  • [48] On The Shape of Circular Dependencies in Java']Java Programs
    Al-Mutawa, Hussain A.
    Dietrich, Jens
    Marsland, Stephen
    McCartin, Catherine
    2014 23RD AUSTRALASIAN SOFTWARE ENGINEERING CONFERENCE (ASWEC), 2013, : 48 - 57
  • [49] Error Detection in Concurrent Java']Java Programs
    Hughes, Graham
    Rajan, Sreeranga P.
    Sidle, Tom
    Swenson, Keith
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 144 (03) : 45 - 58
  • [50] Ensuring the Integrity of Running Java']Java Programs
    Thober, Mark A.
    Pendergrass, J. Aaron
    Jurik, Andrew D.
    JOHNS HOPKINS APL TECHNICAL DIGEST, 2013, 32 (02): : 517 - 527
12345