Java PathFinder A Translator from Java to Promela

Abstract

Java PathFinder [2], Jpf, is a prototype translator from Java to Promela, the modeling language of the Spin model checker [4]. Jpf is a product of a major effort by the Automated Software Engineering group at NASA Ames to make model checking technology part of the software process. Experience has shown that severe bugs can be found in final code using this technique [1], and that automated translation from a programming language to a modeling language like Promela can help reducing the effort required.

Jpf allows a programmer to annotate his Java program with assertions and verify them using the Spin model checker. In addition, deadlocks can be identied. An assertion is written as a call to an assert method dened in a predened Java class, the Verify class. The argument to the method is a boolean Java expression over the state variables. The Verify class contains additional tem- poral logic methods which allow to state temporal logic properties about static variables. Hence Java itself is used as the specication language. An application of Jpf is described elsewhere in the proceedings [3].

A respectable subset of Java is covered by Jpf, including dynamic object cre- ation, object references asrst class citizens, inheritance, exceptions, interrupts, and perhaps most importantly: thread operations. Among major concepts not translated are: packages, method overloading and overriding, method recursion, strings, and floating point numbers. Finally, the class library is not translated.