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 条
  • [21] Functional Testing of Java']Java Programs
    Benac Earle, Clara
    Fredlund, Lars-Ake
    TRENDS IN FUNCTIONAL PROGRAMMING (TFP 2015), 2016, 9547 : 40 - 59
  • [22] Inlining with traces in java']java programs
    Bradel, Borys J.
    Abdelrahman, Tarek S.
    COMPUTER SYSTEMS SCIENCE AND ENGINEERING, 2012, 27 (04): : 251 - 266
  • [23] Formal techniques for Java']Java programs
    Drossopoulou, S
    Eisenbach, S
    Jacobs, B
    Leavens, GT
    Müller, P
    Poetzsch-Heffter, A
    OBJECT-ORIENTED TECHNOLOGY, PROCEEDINGS, 2000, 1964 : 41 - 54
  • [24] Slicing concurrent Java']Java programs
    Chen, ZQ
    Xu, BW
    ACM SIGPLAN NOTICES, 2001, 36 (04) : 41 - 47
  • [25] The Use of Overloading in JAVA']JAVA Programs
    Gil, Joseph
    Lenz, Keren
    ECOOP 2010: OBJECT-ORIENTED PROGRAMMING, 2010, 6183 : 529 - 551
  • [26] Formal techniques for Java']Java programs
    Jacobs, B
    Leavens, GT
    Müller, P
    Poetzsch-Heffter, A
    OBJECT-ORIENTED TECHNOLOGY, 1999, 1743 : 97 - 115
  • [27] Interactive visualization of Java']Java programs
    Gestwicki, P
    Jayaraman, B
    IEEE 2002 SYMPOSIA ON HUMAN CENTRIC COMPUTING LANGUAGES AND ENVIRONMENTS, PROCEEDINGS, 2002, : 226 - 235
  • [28] A Translator of Java']Java Programs to TADDs
    Rataj, Artur
    Wozna, Bozena
    Zbrzezny, Andrzej
    FUNDAMENTA INFORMATICAE, 2009, 93 (1-3) : 305 - 324
  • [29] Verification of Java']Java programs with generics
    Stenzel, Kurt
    Grandy, Holger
    Reif, Wolfgang
    ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGS, 2008, 5140 : 315 - 329
  • [30] Slicing concurrent Java']Java programs
    Zhao, JJ
    SEVENTH INTERNATIONAL WORKSHOP ON PROGRAM COMPREHENSION, PROCEEDINGS, 1999, : 126 - 133
12345