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 条
  • [1] A practical method for watermarking Java']Java programs
    Monden, A
    Iida, H
    Matsumoto, K
    Inoue, K
    Torii, K
    24TH ANNUAL INTERNATIONAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COSPSAC 2000), 2000, 24 : 191 - 197
  • [2] An automatic method for refactoring Java']Java programs
    Yamazaki, S
    Nagata, M
    KNOWLEDGE-BASED SOFTWARE ENGINEERING, 2002, 80 : 167 - 172
  • [3] Combined concept location method for Java']Java programs
    Liu, Dapeng
    Xu, Shaochun
    COMPSAC 2007: THE THIRTY-FIRST ANNUAL INTERNATIONAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE, VOL II, PROCEEDINGS, 2007, : 29 - +
  • [4] DynAlloy as a formal method for the analysis of Java']Java programs
    Galeotti, Juan P.
    Frias, Marcelo F.
    SOFTWARE ENGINEERING TECHNIQUES: DESIGN FOR QUALITY, 2006, 227 : 249 - +
  • [5] SCJ-Circus: Specification and refinement of Safety-Critical Java']Java programs
    Miyazawa, Alvaro
    Cavalcanti, Ana
    Wellings, Andy
    SCIENCE OF COMPUTER PROGRAMMING, 2019, 181 : 140 - 176
  • [6] A Deep Method Renaming Prediction and Refinement Approach for Java']Java Projects
    Liang, Jiahui
    Zou, Weiqin
    Zhang, Jingxuan
    Huang, Zhiqiu
    Sun, Chenxing
    2021 IEEE 21ST INTERNATIONAL CONFERENCE ON SOFTWARE QUALITY, RELIABILITY AND SECURITY (QRS 2021), 2021, : 404 - 413
  • [7] Proposal of a method to support testing for Java']Java programs with UML
    Katayama, T
    Yabuya, Y
    12TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE, PROCEEDINGS, 2005, : 533 - 540
  • [8] Specifying and checking method call sequences of Java']Java programs
    Cheon, Yoonsik
    Perumandla, Ashaveena
    SOFTWARE QUALITY JOURNAL, 2007, 15 (01) : 7 - 25
  • [9] Changing Java']Java programs
    Eisenbach, S
    Sadler, C
    IEEE INTERNATIONAL CONFERENCE ON SOFTWARE MAINTENANCE, PROCEEDINGS: SYSTEMS AND SOFTWARE EVOLUTION IN THE ERA OF THE INTERNET, 2001, : 479 - 487
  • [10] On the visualization of Java']Java programs
    Eichelberger, H
    von Gudenberg, JW
    SOFTWARE VISUALIZATION, 2002, 2269 : 295 - 306
12345