Abstract
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]. © IFIP International Federation for Information Processing 2007.
Cite
CITATION STYLE
Grandy, H., Stenzel, K., & Reif, W. (2007). A refinement method for Java programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4468 LNCS, pp. 221–235). Springer Verlag. https://doi.org/10.1007/978-3-540-72952-5_14
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
