A Refinement Method for Java Programs

Holger Grandy, Kurt Stenzel, Wolfgang Reif

A Refinement Method for Java Programs

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 approach with the verification of a MCommerce application for buying movie tickets using a mobile phone written in J2ME. The approach uses the interactive theorem prover KIV.
published 10.12.2006 in: Universit├Ąt Augsburg, Technical Report 2006-29 Technical Report, Institute of Computer Science, University of Augsburg, December 2006