Executable JVM model for analytical reasoning: A study
To study the properties of the Java Virtual Machine (JVM) and Java programs, our research group has produced a series of JVM models written in a functional subset of Common Lisp. In this paper, we present our most complete JVM model from this series, namely, M6, which is derived from a careful study of the J2ME KVM [Connected Limited Device Configuration (CLDC) and the K Virtual Machine, http://java.sun.com/products/cldc/] implementation. On the one hand, our JVM model is a conventional machine emulator. M6 implements dynamic class loading, class initialization and synchronization via monitors. It executes most J2ME CLDC Java programs that do not use any I/O or floating point operations. Engineers may consider M6 an implementation of the JVM. The June 2003 version is implemented with around I OK lines of Lisp in 28 modules. On the other hand, M6 is novel because it allows for analytical reasoning in addition to conventional testing. M6 is written in an applicative (side-effect free) subset of Common Lisp, for which we have given precise meaning in terms of axioms and inference rules. Properties of M6 and its bytecoded programs can be expressed as formulas and proved as theorems. Proofs are constructed interactively with a mechanical theorem prover. Its concreteness, completeness, executability and mechanized reasoning support make our model unique among JVM models. We argue that our approach of building an executable model of the system with an axiomatically described functional language can bring benefits from both the testing and the formal reasoning worlds. (c) 2005 Elsevier B.V. All rights reserved.
jvm model virtual machine bytecode verification simulator formal methods program verification software specification