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 条
  • [31] A characterization of traces in Java']Java programs
    Bradel, BJ
    Abdelrahman, TS
    PLC '05: PROCEEDINGS OF THE 2005 INTERNATIONAL CONFERENCE ON PROGRAMMING LANGUAGES AND COMPILERS, 2005, : 87 - 93
  • [32] Modeling Java']Java programs for diagnosis
    Mateis, C
    Stumptner, M
    Wotawa, F
    ECAI 2000: 14TH EUROPEAN CONFERENCE ON ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2000, 54 : 171 - 175
  • [33] Profiling Java']Java Programs for Parallelism
    Hammacher, Clemens
    Streit, Kevin
    Hack, Sebastian
    Zeller, Andreas
    2009 ICSE WORKSHOP ON MULTICORE SOFTWARE ENGINEERING (IWMSE), 2009, : 49 - 55
  • [34] Visualizing the execution of Java']Java programs
    De Pauw, W
    Jensen, E
    Mitchell, N
    Sevitsky, G
    Vlissides, J
    Yang, JH
    SOFTWARE VISUALIZATION, 2002, 2269 : 151 - 162
  • [35] Concurrency and synchronization in Java']Java programs
    Moir, M
    Shavit, N
    Vitek, J
    SCIENCE OF COMPUTER PROGRAMMING, 2005, 58 (03) : 291 - 292
  • [36] Understanding the behavior of Java']Java programs
    Systä, T
    SEVENTH WORKING CONFERENCE ON REVERSE ENGINEERING - PROCEEDINGS, 2000, : 214 - 223
  • [37] Algorithmic Debugging of Java']Java Programs
    Caballero, R.
    Hermanns, C.
    Kuchen, H.
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 177 : 75 - 89
  • [38] Formal Techniques for Java']Java Programs
    Leavens, GT
    Drossopoulou, S
    Eisenbach, S
    Poetzsch-Heffter, A
    Poll, E
    OBJECT-ORIENTED TECHNOLOGY, PROCEEDINGS, 2002, 2323 : 30 - 40
  • [39] No Java']Java without caffeine -: A tool for dynamic analysis of Java']Java programs
    Guéhéneuc, YG
    Douence, R
    Jussien, N
    ASE 2002: 17TH IEEE INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, 2002, : 117 - 126
  • [40] Analysis of Java']Java Programs using Joana and Java']Java SDG API
    Kumar, Ranjan
    Panda, Subhrakanta
    Mohapatra, Durga Prasad
    2015 INTERNATIONAL CONFERENCE ON ADVANCES IN COMPUTING, COMMUNICATIONS AND INFORMATICS (ICACCI), 2015, : 2402 - 2408
12345