I (will

Software
be Tools
inserted byfor theTechnology
editor) Transfer manuscript No.

Model Checking Java Programs

Using Java PathFinder
Klaus Havelund, Thomas Pressburger

NASA Ames Research Center,

Recom Technologies,
Moffett Field, California, USA.
e-mail: {havelund, ttp}©ptolemy, arc. nasa. gov
url: http ://ase. arc. nasa. gov/{havelund, ttp}

March 12, 1999

Abstract. This paper describes a translator called JAVA

PATHFINDER from JAVA to PROMELA, the "program-
ming language" of the SPIN model checker. The purpose
is to establish a framework for verification and debug-

ging of JAVA programs based on model checking. This

work should be seen in a broader attempt to make formal
methods applicable "in the loop" of programming within
NASA's areas such as space, aviation, and robotics. Our
main goal is to create automated formal methods such
that programmers themselves can apply these in their
daily work (in the loop) without the need for specialists
to manually reformulate a program into a different no-
tation in order to analyze the program. This work is a
continuation of an effort to formally verify, using SPIN,
a multi-threaded operating system programmed in LISP
for the Deep-Space 1 space craft, and of previous work
in applying existing model checkers and theorem provers
to real applications.

Key words: Program verification- JAVA model check-

ing - SPIN - concurrent programming - assertions -
deadlocks:
 1 Introduction The verification effort consisted of hand translating parts
of the LIsP code into the PROMELA language of SPIN. A
In this paper we describe JAVA PATttFINDER (JPF), a total of 5 errors were identified, a very successful result.
translator from JAVA to PROMELA, the programming It is often claimed that model checkers of today can-
language of the SPIN model checker. The purpose is not handle real sized programs, and consequently can-
to establish a framework for verification and debugging not handle real sized JAVA programs. This is certainly
of JAVA programs based on model checking. The work true. However, there are two aspects that make our ef-
should be seen in a broader attempt to make formal fort worthwhile anyway. First, by providing an abstrac-
methods applicabIe "in the loop" of programming within tion workbench we will make it possible to cut down the
NASA's areas such as space, aviation, and robotics. Our state space of a JAVA program. Second, one can imag-
main long term goal is to create an automated formal ine model checking being applied for unit testing, where
methods workbench for JAVA programming such that one focuses on a single class (or a few classes) and puts
programmers themselves can apply them in their daily this (these) in parallel with an aggressive environment
work (in the loop) without the need for specialists to represented by a number of threads. Finally, JAVA can
manually reformulate a program in a different notation be used as a design Ianguage, just as PROMELA.
in order to analyze it. Few attempts have been made to automatically ver-
The tool we are developing is named after the rover ify programs written in real programming languages.
operating on Mars in 1997 called the "Mars PathFinder". The most recent attempt we can mention is the one re-
Although this mission was generally regarded as a big ported in [2], which also translates JAVA programs into
success, the rover did in fact contain a number of soft- PROMELA, however not handling exceptions or polymor-
ware bugs (causing repeated rebootings and panic at phism as we do. The work in [3] defines a translator from
NASA headquarters) that could potentially have been a concurrent extension of a very limited subset of C++.
found beforehand using proper verification tools. The The drawback of this solution is that the concurrency
JAVA PATttFINDER name is a play on words: it finds the extensions are not broadly used by C++ programmers.
paths of a JAVA program that lead to errors. In [5] is described what is called Extended static check-
JAVA [6, 1] is a general purpose object-oriented pro- ing, a technique for detecting, at compile-time, common
gramming language with built in mechanisms for nmlti- programming errors. The technique uses program ver-
threaded programming [16]. It was originally designed to ification technology, but feels to a programmer like a
support internet programming, but goes well beyond this type checker. By using an underlying automatic theorem
domain. JAVA is a relatively simple language compared prover, the technique is more semantically thorough than
to C++, and it is regarded as a much safer language, decidable static analysis techniques. At the same time,
amongst other things due to its automatic garbage col- by only trying to detect certain kinds of errors, not prove
lection and lack of general pointers. In spite of its sim- the program's correctness, the technique is more auto-
plicity it appears to be a powerful language. matic than program verification. Finally, [4] describes a
SPIN [15] is a verification system that supports the theory of translating JAVA to a transition model, making
design and verification of finite state asynchronous pro- use of static pointer analysis to aid virtual coarsening,
cess systems. Programs are formulated in the PROMELA which reduces the size of the model.
programming language, which is quite similar to an or- A significant subset of JAVA version 1.0 is supported
dinary programming language, except for certain non- by JPF: dynamic creation of objects with data and meth-
deterministic specification oriented constructs. Processes ods, class inheritance, threads and synchronization prim-
communicate either via shared variables or via message itives for modeling monitors (synchronized statements,
passing through buffered channels. Properties to be veri- and the wait and notify methods), exceptions, thread
fied are stated as assertions in the code, or as formulae in interrupts, and most of the standard programming lan-
the linear temporal logic LTL. The SPIN model checker guage constructs such as assignment statements, condi-
can automatically determine whether a program satis- tional statements and loops. However, the translator is
fies a property, and, in case the property does not hold, still a prototype and misses some features, such as pack-
generate an error trace. SPIN also finds deadlocks. ages, overloading, method overriding, recursion, strings,
In an earlier effort we formally verified, using SPIN, floating point numbers, static variables and static meth-
a multi-threaded operating system for a spacecraft [9]. ods, some thread operations like suspend and resume,
The operating system is one component of NASA's New and some control constructs, such as the continue state-
Millennium Remote Agent (RA) [17], an artificial in- ment. In addition, arrays are not objects as they are in
telligence based spacecraft control system architecture JAVA, but are modeled using PROMELA'S own arrays to
launched October 24, 1998, as part of the Deep-Space 1 obtain efficient verification. Finally, we do not translate
mission to an asteroid to validate the potential of arti- the predefined class library.
ficial intelligence, ion propulsion, and other technologies Note that many of these features can be avoided by
for future space crafts. The operating system is imple- small modifications to tim input code. In addition, the
mented in a multi-threaded version of COMMON LISP. tool is currently being improved to cover more of JAVA.
 class HaltException extends Exception{}
Despitethe omissions,
weexpectthecurrentversionof
JPFto beusefulon a largeclass of software. A front- interface BufferInterface {
end to the translator checks that the program is in the
public void put(0bject x);
allowed subset and prints out error messages when not. public Dbject get() throws HaltException;
The translator is developed in COMMON LISP, having a public void halt();
JAVA parser written in MoscowML as front end. Ger- }
ard Holzmann supported our efforts by changing the se- Fig. 1. The JAVABuffer interfaze
mantics for the PROMELA unless construct in order to
simplify the translation of exceptions.
The paper is organized around an example JAVA pro-
as the class, and a collection of methods. One of the con-
gram that has been translated automatically by JAVA
PATHFINDER and verified automatically by SPIN. In Sec- structors is executed when an object is created with the
new construct. Note that the Buffer class has no such
tion 2 we describe this program, a bounded buffer. In
user-defined constructors. The class declares an array of
Section 3 we describe what the resulting PROMELA code
length 3 to hold the objects in the buffer. A cleaner way
looks like. In Section 4 we present an experiment where
of writing this program would be to declare a constant
we seeded 21 errors into the example program, and ran
"final int SIZE = 3" and then refer to SIZE rather
the SPIN model checker on the code generated by JPF.
Section 5 ends with conclusions and suggestions for fu- than to 3 throughout the program. The translator, how-
ture work. ever, currently requires an integer literal as the dimen-
sion of an array. In addition to the array, a couple of
pointers are declared, one pointing to the next fi'ee loca-
tion, and one pointing to the next object to be returned
2 The Bounded Buffer Program
by the get method. The variable usedSlots keeps track
of the current number of elements in the buffer. Finally,
The translation scheme will be illustrated by translation the variable halted will become true when the halt
of a complete, small, but non-trivial JAvA.program that method is called.
covers many of the features of JAVA that we can trans- The three methods of the class are all synchronized
late. After translation by JPF, SPIN can be applied to (note the synchronized keyword). Hence, each of these
prove or disprove that the program satisfies given prop- methods will have exclusive access to the object when
erties stated as assertions in the program, and that it is executed. That is, when one of these methods is called
deadlock free. on the buffer object by a thread, the buffer gets locked
to serve that thread, and it is unlocked again at the end
2.1 The Buffer Class of the method call. The put method takes as parameter
the object to be stored in the buffer and has no return
value (void). It enters a loop testing whether the buffer
The JAVA program that we are interested in verifying
is full (i.e. having 3 elements) in which case it calls the
properties about is a bounded buffer, represented by a
built in wait method. Calling the wait method within
single class. An object of this class can store objects of
a synchronized method suspends the current thread and
any kind (objects of subclasses of the general top level
allows other threads to execute synchronized methods on
class Object). Figure 1 shows the declared interface of
the object. Such another thread can then call the notify
this class. It contains a put method, a get method and
method which will wake up an arbitrarily chosen waiting
a halt method. Typically there will be one or more pro-
thread to continue past its wait () call. The notifyAll
ducer threads that call the put method, and one or more
method wakes up all such waiting threads.
consumer threads that call the get method. The halt
The call of wait is put inside a try construct, which
method can be invoked by a producer to inform con-
is JAVA's exception handling construct. A general try
sumers that it will no longer produce values to the buffer.
construct has the form:
Consumers are allowed to empty the buffer safely after
a halt, but if a consumer calls the get method after the try T
halt method has been called, and the buffer is empty, an catch{El el) C1
exception object of class HaltException will be thrown.
A class is an exception class if it is a subclass of the class catch(E2 en) Cn
Throwable. In particular, class Exception is a subclass finally F
of Throwable.
Figure 2 contains the Buffer class annotated with where each T,C1 ..... Cn, F is a block (a statement or a
line numbers for later reference. A JAVA class is gener- sequence of statements enclosed by {...}) and each Ei is
ally speaking described by a name, a set of data vari- an exception type (class). The body T of the try state-
ables, zero or more constructor methods (with different ment is executed until either an exception is thrown or it
argument types if more than one) with the same name finishes successfully. If an exception is thrown, the catch
 1. class Buffer implements BufferInterface { class Main {
2. protected Object[] array = new Object[3]; public static void main(String[] args) {
3. protected int putPtr = O; Buffer b = new Buffer();
4. protected int getPtr = O; Producer p = new Producer(b);
5. protected int usedSlots = O; consumer c = new Consumer(b);
6. protected boolean halted; }
7.
8. public synchronized void put(0bject x) {
Fig. 3. The JAVA main program
9. while (usedSlots == 3)
10. try {wait();}
11. catch(InterruptedException ex) {};
12. array[putPtr] = x; executing T. interrupt (), which throws an
13. putPtr = (putPtr + I) _ 3; InterruptedException, or T.stop(), which throws a
14. if (usedSlots == O) notifyAllO; ThreadDeath exception. The try construct around the
15. usedSlots++; wait call is supposed to catch exactly such interrupts
16.
from other threads. As we see, nothing is done in this
17.
case (lines 11 and 22), but the try statement is neces-
18. public synchronized Object get()
19. sary in order for the JAVA type checker to accept the
throws HaltException{
20. while (usedSlots == 0 & !halted) program. We shall later see a real use of exceptions. One
21. of the main results in this paper is that we can in fact
try {wait();}
22. catch(InterruptedException ex) {}; prove properties of programs that throw exceptions.
23. if (usedSlots == O) { When finally the put method gets past the while
24. throw(new HaltException()); loop, it is known that the buffer has free space, and the
25. }; insertion of the new object can be completed. In case
26. Object x = array[getPtr]; the buffer was in fact empty, all waiting consumers are
27. array[getPtr] = null; notified.
28. getPtr = (getPtr + 1) Z 3; The get method is a little bit more complicated be-
29. if (usedSlots == 3) notifyAll();
cause it also takes into account whether the buffer has
30. usedSlots--;
31. been halted. Basically, it will wait uutil there is some-
return x;
32. thing in the buffer, and return this element, unless the
33. buffer is empty and at the same time ha_ been halted.
34. public synchronized void halt(){ In this case, a HaltException is thrown. Otherwise, the
35. halted = true; next buffer element is returned, and producers are noti-
36. notifyAll(); fied if the buffer beforehand was full, in which case they
37. } may be waiting.
38. }

Fig. 2. The JAVA Buffer class 2.2 Setting up an Environment

In order to verify properties about this class, without

clauses are examined from top to bottom in order to find looking at a complete application within which it oc-
one where the thrown exception is of the corresponding curs, we can create a small application using the buffer.
class Ei or of a subclass thereof. If such a catch is found, We say that we set up an environment consisting of a
the corresponding block Ci is executed. If no appropri- number of threads accessing the buffer, and then we
ate catch is found, the exception "flows out" of the try prove properties about this small system. This can be
statement into an outer try that might handle it. There regarded as unit testing the buffer. Concretely, we shall
can be any number of catch clauses in a try including define two thread classes: a Producer and a Consumer
none. If no catch clause in the method catches the ex- class, and then start the whole system as shown in the
ception, the exception is thrown to the code that invoked main method in Figure 3.
this method. If a finally clause is present in a try, its First, in order to illustrate the translator's capabili-
code is executed after all other processing in the try is ties to translate inheritance, we define the objects that
complete. This happens no matter how the completion are to be stored in the buffer, see Figure 4. A class
was achieved, whether normally, through an exception, Attribute is defined, which contains one integer vari-
or through a control flow statement like return. able. The constructor method with the same name as
Normally an exception is thrown explicitly within a the class takes a parameter and stores it in this variable.
thread using the throw(e) statement, where e is an ex- The class httrData extends this class with another field,
ception object (a normal object of an exception class and defines a constructor, which takes two parameters,
which may include data and methods). However, one and then calls the super class constructor with the first
thread S may throw an exception in another thread T by parameter.
 class Attribute{ class Producer extends Thread {

public int attr; private Buffer buffer;

public Attribute(int attr){ public Producer(Buffer b) {

this.attr = attr; buffer = b;
} this.start();
} }

class AttrData extends Attribute{ public void run() {

public int data; for (int i = O; i < 6; i++) {

AttrData ad = new AttrData(i,i*i);
public AttrData(int attr,int data){ buffer.put(ad);
super(attr); yield();
this.data = data; };
} buffer.halt();
}
Fig. 4. The JAVA Attribute and AttrData classes

class Consumer extends Thread {

The producer and consumer threads that are actu- private Buffer buffer;
ally going to use the buffer are defined in Figure 5. The
Producer class extends the Thread class, which means public Consumer(Buffer b) {
that it must have a run method, which is then executed buffer = b;

when an object of this class is started with the start this.start();

}
method. As can be seen, the constructor of the class in
fact calls this start method in addition to storing locally
public void run() {
the buffer for which elements will be produced. The run
int count = O;
method adds 6 AttrData objects to the buffer, with at- AttrData[] received = new AttrData[lO];
tributes 0... 5 (in that order) and squares as data, and try{
then calls the halt method on the buffer. while (count < 10){
The Consumer class also extends the Thread class. received[count] = (AttrData)buffer.getO;
The run method stores all received objects in the count++;

received array (or at most 10 of them). Note how the }

receiving loop is written inside a try construct, which }
catches and prevents a HaltException from going fur- catch(HaltException e){};

ther. Verify.assert(count == 6);

for (int i = O; i < count; i++){

Verify.assert(received[i].attr == i);}
2.3 Property Specifications

JPF allows a programmer to annotate his JAVA program Fig. 5. The JAVA Producer and Consumer classes
with assertions and verify them using the SPIN model
checker. In addition, deadlocks can be identified. An as-
class Verify{
sert statement is expressed as a call to the static method
public static void assert(boolean b){
assert in the Verify class shown in Figure 6. The fact
if (!b)
that it is static means that we can call this method di-
System.out.println("assertion broken");
rectly using the class name Verify as prefix, without }
making an object instance first. The body of this method
is of no real importance for the verification since only
Fig. 6. The JAVA Verify class
the call of this method (and not its definition) will be
translated into a corresponding PROMELA assert state-
ment. A meaningful body, like print!ng an error message
as in this example, can be useful during normal testing One can consider other kinds of Verify methods, in
though, but it will not be translated into PROMELA. general methods corresponding to the operators in LTL,
The first assertion in Figure 5 states that the con- the linear temporal logic of SPIN. Since these methods
sumer receives exactly 6 elements from the buffer. The can be called wherever statements can occur, this kind of
second assertion within the for loop states that the re- logic represents what could be called an embedded tempo-
ceived elements are the correct ones (at least wrt. the ral logic. As an example, one could consider a statement
attr value). of the form: Verify.eventually(count == 6) inserted
 #define Index byte
#define Attribute 6
#define MAX_OBJECT 7
#define AttrData 7

typedef Attribute_Class{
int attr;
#define create object(c,i)
};
(c*100 + i)
Attribute_Class Attribute_Obj[MAX_OBJECT];
Index Attribute_Next = O;
#define get_class(x)
(x/100)
typedef AttrData_Class{
int attr;
#define get_index(x)
int data;
(x - ((x/100)*t00))
};
AttrData_Class AttrData_Obj[MAX_OBJECT]; Fig. 8. GenerM object re_rence operations
Index AttrData_Next = O;

Fig. 7. Object arrays _rthe Attribute and AttrData classes

A particular object is now referenced by an object ref-

erence containing information about which class it con-
as the second statement of the consumer run method. cerns (and thereby which array) and which instance (in-
The major advantage of this approach is that we do dex in the array) it concerns. Because PROMELA'S record
not need to change the JAVA language, or parse spe- concept (typedefs) is not flexible enough for our needs
cial "specification comments". JAVA itself is used as the (e.g., field access cannot be applied to a conditional ex-
specification language. Note, however, that at this point, pression) we have decided to represent an object ref-
only the assert method is supported. erence (c,i) as the integer c * 100 + i. The operations
(macros) for dealing with these calculatious are shown
in Figure 8. Each class is given a unique identification
3 Translation which is a number, for example class Attribute is given
number 6.
In order to access the variables in these arrays, macros
3.1 Classes, Inheritance and Object Creation are defined as shown in Figure 9. These macros are pre-
fixed with tlle name of the class that defines the vari-
The general principle behind the translation is the fol- able, which is statically decidable in JAVA at the point
lowing. A JAVA class basically consists of data variables where the variable is accessed (in contrast to method
and methods. For each new creation of an object, a new calls). However, because JAVA supports polymorphism
set of data variables, a data area, is allocated, and the where an object may belong to a subclass of the stati-
methods of that object will then work on this newly allo- cally declared class (for example if it is a parameter to a
cated area. Hence, at any point in time a set of data areas method) we need to define these variable accessors such
will have been allocated, one for each object not garbage that they access the right array. For example, the macro
collected. We shall model tile set of data areas of a class httribute_get_attr for reading the attr variable de-
by an array of records (typedef's in SPIN terminology), fined in the Attribute class is defined as a conditional
one record for each data area. An index variable will expression over the subclasses.
point to the next free record in the array, initially having Both classes have constructors which will be executed
the value 0 (first record in the array). Method definitions when creating new objects. For example, the JAVA ex-
are mapped into macro definitions, and method calls are pression "new httrData(2,4)" will cause a call of the
mapped into applications of macros. Note that the trans- constructor, which in turn will call the constructor of
lated code shown is tile unedited PROMELA code gener- the super class: "Attribute (2)". Constructors are mod-
ated by tile translator (except for a couple of omissions). eled as macros as shown in Figure 10 (slightly simpli-
For illustration, we start with the translation of the fied for presentation purposes; the real translation also
simplest classes, namely Attribute and httrData, which takes into account variable initializations occurring to-
have no methods, but which show inheritance. Figure 7 gether with variable declarations). The parameter obj
shows the data areas for the two classes. For each class will be an object reference denoting the object being
C an array named C_0bj is defined of size MAX_0BJECT constructed.
and of type C_Class. In addition, a pointer C_Index to The construction of a new object such as for ex-
the next fi'ee data area (object) is declared. Because the ample the JAVA statement "x = new httrData(2,4)"
AttrData class inherits from the Attribute class, it in- is mapped into the sequence of PROMELA statements
cludes the attr variable in addition to the data variable. shown in Figure 11 (slightly simplified here with respect
Note that this translation puts a limit (MAX_0BJECT) to the treatment of the variable x): one can see how
on the number of objects that can be created of a class. the x is bound to a reference, the next-pointer is incre-
 #define undefined 0 typedef Buffer_Class{
int LOCK;
#define Attribute_get_attr(obj) byte WAITING;
(get_class(ob]) == AttrData -> chan WAIT = [0] of {bit};
AttrData_Dbj[get_index(obj)].attr : ObjRef array[3];
(get_class(obj) == Attribute -> int putPtr;
Attribute_Obj[get_index(obj)].attr : int getPtr;
undefined)) int usedSlots;
bit halted;
#define Attribute,set_attr(obj,value) };
if
Fig. 12. Object type _r the Buffer class
:: get_class(obj) == AttrData ->
AttrData_Dbj[get_index(obj)].attr = value
:: get_class(obj) == Attribute -> #define Buffer_any_WAITING(obj)
Attribute_Obj[get_index(obj)].attr = value Buffer_Obj[get_index(obj)].WAITING > 0
fi

#define Buffer_incr_WAITING(obj)
#define AttrData_get_data(obj) Buffer_Obj[get_index(obj)].WAITING++
AttrData_Obj[get_index(obj)].data

#define Buffer_decr_WAITING(obj)
#define AttrData_set_data(obj,value) Buffer_Obj[get_index(obj)].WAITING--
AttrData_Obj[get_index(obj)].data = value
Fig. 13. Operations on WAITING
Fig. 9. Variable accessors _rthe Attribute and AttrData classes

#define Attribute_constr(obj,attr)
ables LOCK, WAITING and WAIT used for managing ob-
Attribute_set_attr(obj,attr);
ject locking and release. The LOCK variable will at any
#define AttrData_constr(oBj,attr,data) time either be null (a negative integer) or it will be the
Attribute_constr(obj,attr); thread id of the thread that currently is executing a syn-
AttrData_set_data(obj,data); chronized method on the object (actually a non-negative
PROMELA process id). Hence, once this field is set to a
Fig. 10. Constructors _rthe Attribute and AttrData classes
proper thread id by a thread that calls a synchronized
method, only the thread with this thread id is allowed to
atomic{
operate on the object. When the call of the synchronized
x = create_object(AttrData,AttrData_Next);
method terminates, the lock is released by setting it to
AttrData_Next++
}; null again. Note that a synchronized method must be
allowed to call other synchronized methods on the same
AttrData_constr(x,2,4);
object without causing blocking.
Fig. 11. W rans|ation ofx = new AttrData(2,4)
The variables WAITING and WAIT are used to man-
age threads that call the wait, notify, and notifyAll
methods on the object. A thread that calls wait() will
mented, and the constructor is applied to the reference first unlock the object, and then try to read a value on
now stored in x.
the zero place channel WAIT. A zero place channel in
PROMELA is used to model rendezvous communication,
3.2 Synchronization on Objects hence some other thread must send a value on this chan-
nel in order for the calling thread to be released. At any
The Buffer class is more complicated because it con- time, all threads that are waiting to get access to the
tains methods, and because these in addition are syn- object are waiting on this channel. Each time a thread
chronized, which means that they must have exclusive calls the wait () method on the object, the WAITING vari-
access to the object when executing. That is, only one able is additionally incremented, and conversely decre-
thread at a time may execute any synchronized method mented when released. Hence, the value of this variable
on the same object. Therefore, the translation must pro- will always be the number of threads waiting on the ob-
vide a locking mechanism with which one can lock an ject. The variable is used when notifyAll is called by a
object to serve a particular thread that calls a synchro- thread, and all waiting threads have to be released: we
nized method on the object. For that purpose some extra need to know how many times the WAIT channel must
variables are inserted into the data area of each object, be signaled. The operations on the WAITING variable are
as shown in Figure 12. In addition to the variables de- shown in Figure 13.
clared in the class (note that JAVA arrays are modeled Locking and unlocking an object is implemented by
directly as PROMELA arrays), it contains the three vari- the operations shown in Figure 14. Locking an object
 #define continue 0
#define this _pid

#define Buffer_wait(obj)
#define Buffer_lock(obj)
atomic{ atomic{

Buffer_get_LOCK(obj) == null -> {

Buffer_set_LOCK(obj,this)} Buffer_unlock(obj);
Buffer_incr_WAITING(obj);

#define Buffer_unlock(obj) Buffer_get_WAIT(obj)?continue

Buffer_set_LOCK(obj,null) }
unless{
Fig. 14. Operations _rlocking and unlocking objects d_step{

get_this_EXN > 0 ->

Buffer_decr_WAITING(obj)
}
is done when a thread calls a synchronized method on
};
an object which the thread has not already locked. First
Buffer_lock(obj)
the thread waits until the lock becomes free (no other }
thread has locked it), which is the case when the LOCK unless {a_finally(Buffer_lock(obj))}
field becomes null. Note that in PROMELA, an equality
is a statement that is executable only when the equality #define Buffer_notify(obj)
holds, and hence blocks until this is the case. Then, in an atomic{

atomic move, the thread locks the object by assigning the if

value of '%his" to the LOCK field, where "this" denotes :: Buffer_any_WAITING(obj) ->
Buffer_get_WAIT(obj)!continue;
the thread id of the current thread ("this" is defined as
Buffer_decr_WAITING(obj)
_pid, which in PROMELA refers to the process id of the
:: else -> skip
currently executing process). Unlocking an object just
fi}
corresponds to setting the LOCK field to null.
Finally, the macros modeling the wait, notify and #define Buffer_notifyAll(obj)
notifyAll methods are shown in Figure 15. The atomic{
Buffer_wait macro models the wait method. Ignore do
for a moment tim unless constructs. When called, it :: Buffer_any_WAITING(obj) ->

first unlocks the object, because other threads should Buffer_get_WAIT(obj)!continue;

Buffer_decr_WAITING(obj)
now have access to perhaps later call notify. Then the
:: else -> break
WAITING field is increased, and finally the thread starts
od}
waiting for a signal (the value 0) on the WAIT channel.
When the thread is woken up by a notify or notifyAll, Fig. 15. The oper_ions wait, notify and notifyAll

it locks the object again (first occurring call of

Buffer_lock(obj)) in order to continue with exclusive
access to the object (note that wait can only be called
within a synchronized context in JAVA).
The Buffer_notify macro signals the WAIT chan-
nel in case there are threads waiting for a signal. The such an interrupt occurs. Then (due to the new seman-
Buffer.notifyAll macro does this as long as there are tics of the PROMELA unless construct, see Section 3.5)
threads waiting. Note that this happens atomically so the inner unless construct will be triggered since, as we
that no new threads can join the waiting threads during shall see, this implies that get_this_EXN becomes bigger
the notification. than zero. This causes the WAITING variable to be decre-
Now we explain the unless constructs in the mented, which is necessary because the Buffer_notify
Buffer_wait macro. This extra complication is caused and Buffer_notifyAll macros normally do this (and
by the fact that another thread can either interrupt or now have not had the chance to do it). Next, because
stop a thread that is waiting. Recall that such an inter- the waiting thread may have code in finally constructs
rupt or stop is like an exception being thrown inside the that must be executed before termination (not shown
(perhaps waiting) thread being interrupted or stopped. here), it is necessary to lock the object again before stop-
We shall later explain exceptions in more detail, but here ping such that this finalize code can be executed with
it suffices to say that in case such an exception is thrown, exclusive access to the object. This is done by the out-
the waiting thread must be released immediately; this ermost unless construct. It was necessary to introduce
occurs because the conditions of the two unless con- two unless constructs since the interrupt may also ar-
structs become true. rive after the thread has been woken up, but while it is
Suppose that the waiting thread is blocked in the waiting for the lock to be released; that is, it is waiting
"Buffer_get_WAIT (obj)?continue" statement, and that in the first occurring Buffer_lock(obj) statement.
 #define Buffer_halt(obj) proctype Producer_Thread(ObjRef obj){

if {
int Producer_run_i;
:: Buffer_get_LOCK(obj) == this ->
Buffer_halt_code(obj) ObjRef Producer_run_ad;

:: else -> ObjRef Buffer_put_ex;

Producer_run_i = O;
Buffer_lock(obj);
do
try(Buffer_halt_code(obj))
unless {d_finally(Buffer_unlock(obj))} :: (Producer_run_i < 6) ->

fi atomic{
Producer_run_ad =

#define Buffer_halt_code(obj) create_object(AttrData,AttrData_Next);

Buffer_set_halted(obj,true); AttrData_Next++};

Buffer_notifyAll(obj) AttrData_constr(Producer_run_ad,
Producer_run_i,
Fig. 16. Trans]ation ofthe halt method (Producer_run_i * Producer_run_i));

Buffer_put(Producer_get_buffer(obj),
Producer_run_ad);
Producer_run_i = (Producer_run_i + i);
3.3 Methods
:: else -> break

od;
In order to illustrate how methods are modeled, we illus- Buffer_halt(Producer_get_buffer(obj));
trate the simplest one, namely the halt method. A syn- }
chronized method M in a class ¢ is defined in two parts: unless {get_this_EXN > O}
a ¢_M macro dealing with object locking, and a C_M_code
macro containing the actual code of the method. For Fig. 1T. The Producer run method
non-synchronized methods there is no such distinction.
This is shown for the synchronized halt method in Fig-
ure 16. In general, a method call is translated into a call
of the ¢_M macro with parameters corresponding to the
method parameters. In the case of halt, the method is The process takes as parameter its own object ref-
parameterless, hence only tile object reference of the ob- erence. Notice how local variables in called methods are
ject upon which the method is called is given as parame- declared as global variables in the process. For example,
ter. The macro tests whether the object is already locked the variable ex in the put method that binds the caught
by the calling thread, in which case the actual code, exception in the try statement (Figure 2) is declared
C_M_code, is executed. This models the situation where at this point. This is necessary because PROMELA does
this method is called by another synchronized method, not support local variables (nor does it in the new inline
hence the object is already locked. In case the object procedures that PROMELA got recently). This solution
is not locked by the calling thread, an attempt is made of course prevents the translation of recursive methods,
to lock it (Buffer_lock (obj) ), and after successful lock- but it is efficient with respect to verification time since
ing, the code is executed. The try macro models tile try we don't need to maintain a call stack (and represents
construct of JAVA and models the fact that the object what one normally would do in a hand translation). An-
must always be unlocked (Buffer_unlock(obj)) when other possibility is to translate methods into proctypes,
leaving the method, also in the case where an exception as suggested in [15], but experiences during earlier work
is raised during execution of the code. suggested that this would be inefficient, see [9]. The while
loop is translated into PROMELA'S do ... od construct

in a very straight forward way.

3.4 Threads
Note in Figure 17 how the object reference to the
It remains to explain how things are put together by buffer in the buffer variable declared inside the Producer
translating the main method and the threads that it class is accessed and passed as argument to the put and
starts. First, we describe how the thread classes Producer halt methods. This models the dot-notation in JAVA for
and Consumer are translated. We focus on the Producer. accessing methods in an object. Surrounding the pro-
Thread classes are translated in a similar manner to ducer thread code is an unless construct, which is sup-
other classes, with the addition that the run method posed to catch any exceptions thrown and not caught
is translated into a PROMELA process type (proctype), by the user program. This will be explained in the next
that can then be started using the PROMELA run state- section. Finally, Figure 18 shows the translation of the
ment, whenever a corresponding JAVA thread is started Producer object constructor. It shows how the buffer
with the JAVA start method. Figure 17 shows the trans- variable is initialized with the argument, and how the
lation of the run method of the Producer class of Figure process is started, corresponding to the "this. start ()"
5. call.
 #define Producer_constr(obj,b) typedef Consumer_Class{
Producer_set_buffer(obj,b); ObjRef EXN;
run Producer_Thread(obj); ObjRef buffer;
};
Fig. 18.The Producerconstructor
Fig.19.The Consumerobjecttype

3.5 Exceptions #define exn_Exception

(get_class(get_this_EXN)== Exception
JAVA exceptions are complicated when considering all lexn_InterruptedException
[exn_HaltException)
the situations that may arise, such as method returns
in the middle of try constructs, the finally construct, Fig.20. The exn_xception predicate
interrupts (which are exceptions thrown from one thread
to another) of threads that have called the wait method,
#define dotted_throw(obj,exn)
and the fact that objects have to be unlocked when an
set_EXN(obj,exn)
exception is thrown out of a synchronized method. We
shall try to illustrate our solution. #define throw(exn)
PROMELA'S unless construct seems very closely re- dotted_throw(obj,exn)
lated to an exception construct, except for the fact that
it works "outside in" instead of "inside out", the latter #define stop(obj)
being the case for exceptions. As an example consider dotted_throw(obj,THREAD_DEATH)
the JAVA statement (assuming some variable x): Fig.21. Operations
_rthrowing exceptions
try{
try{throw(new Exception() ) ;}
catch(Exception e){x = i;} defined exception class. Hence, an exception may con-
} tain data and methods. The throw(e) statement takes
catch(Exception e){x = 2;} an exception object reference e as argument, and in our
model we translate that into a store of that object ref-
The result of executing this statement should be that
x is assigned to 1, hence (only) the inner catch is invoked erence in a special variable, EXN, in tlie data area of
when the exception is thrown. In contrast, consider a re- ' the thread (potentially the main program) where it has
been thrown. All the unless constructs in the thread will
lated PROMELA statement, where now an EXN variable
test on this variable to see if it becomes different from
(initially 0) has been introduced. When this variat)le be-
null. The data area for the Consumer class is shown
comes positive it is regarded as if an exception has been
thrown: in Figure 19. There are corresponding macros for ac-
cessing this variable. There are macros get_EXN(obj)
{ and set_EXN(obj ,value) for accessing this variable of
{EXN = i} a thread identified by obj. In addition, the macros
unless {EXN > 0 -> x = I} get_this_EXN and set_this_EXN willaccessthe EXN vari-
} able of this thread.
unless {EXN > 0 -> x = 2} For each exception class E, there is a predicate exn_E
which evaluates to true if the EXN variable contains an
The effect of this statement will be that x is as-
signed to 2. Hence, the outermost unless construct is exception object of that class or a subclass thereof. For
invoked when EXN becomes positive. Gerard Holzmann example, Figure 20 shows this predicate for the built in
has been very helpful to us by implementing a -J option Except ion class. Recall that the ttaltExcept ion was de-
fined as a subclass thereof, as is InterruptedException.
(J for JAVA) in the verifier that changes the semantics
of PROMELA in such a way that unless constructs are Exception throwing is mainly modeled by the macros
interpreted "inside out". This still leaves a second issue: shown in Figure 21. The dotted_throw macro throws
that as soon as the inner unless is chosen (executing an exception at a particular object given as parame-
the inner EXN > 0), then the outer is invoked (since EXN ter. This allows one thread to throw an exception at

> 0 is still true) and x gets the value 2 anyway. Hence, another thread, causing that other thread's EXN variable
to be set. The throw macro throws an exception to the
we have to prevent that kind of behavior. Note that the
above PROMELA code needs some modifications to ac- object identified by the free variable obj which is this
tually "work" because if it is the last statement in "P" current thread object. Finally, calling "T. stop()" in a
within the statement "P unless Q" that makes "Q" ex- JAVA program corresponds to throwing the predefined
ecutable, then "0" will actually not get executed. THREAD_DEATH exception object to the T object.
Recall that a JAVA exception is an object of one of We shall now explain how exceptions are caught.
the exception classes, either one of the built in or a user Consider a try statement of the form:
 #define try(s)
{ try(Buffer_wait(obj))
unless { {s;exit_to_final;skip}

if
#define exit_to_final
:: catch(exn_InterruptedException,
throw(EXIT)
Buffer_get_ex,skip)
fi};
#define catch(exn_E,x,s)
}
catch_cond(exn_E,x) -> s;exit_to_final
unless {finally(skip)};

Fig. 22. Trans|ation ofthe try statementin the get method #define catch_cond(exn_E,e)

d_step{
(exn_E)
->
try T
e = get_this_EXN;
catch(El el) Cl
set_this_EXN(NO_EXN)
catch(E2 e2) C2
}

catch(En en) Cn
#define finally(s)
finally F final_cond -> s;exit_final;skip

A JAVA statement of this form is translated into a

#define final_cond
PROMELA statement of the following form using macros d_step{
defined in Figure 23, and where a prime (') after a block get_this_EXN > 0 ->
indicates its translated version: if

:: get_this_EXN == EXIT ->

{ try(T') set_this_EXN(N0_EXN)

unless { :: else ->

if set_this_EXN(- get_this_EXN)

:: catch(exn_El,el,Cl') fi}
:: catch(exn_E2 & !exn_El,e2,C2')
#define exit_final
set_this_EXN(- get_this_EXN)
catch(exn_En & !exn_El & !exn_E2 &
... _ !exn_En-l,en,Cn') Fig. 23. Operations _rcatching exceptions

fi}
}
unless {finally(F')}
be accessible within the block to be executed. Note also
how the EXN variable is zeroed to the predefined NO_EXN
For example, the try construct in the get method
value in order to avoid outer unless constructs being
in Figure 2 is translated into the PROMELA code in Fig-
triggered, as already discussed earlier on page 10.
ure 22. The general idea behind this translation is that
the inner unless construct catches any exceptions which The finally (s) macro defines when the outer unless
match any one of the exception predicates exn v.1 ... construct should be triggered, namely when f inal_cond
exn_En, and that the outer unless construct models the becomes executable. The f inal_cond macro is executable
finally construct in JAVA: the block F must be exe- whenever there is some exception object reference in the
cuted no matter what as the last thing. For example, EXN variable (it is bigger than 0). Note that we reset this
in the case where for example C l' itself throws a new to 0 (N0_EXN) whenever an exception is caught at an in-
exception, the F still has to be executed before that ex- ner level so that this outer final construct will not get
ception can be thrown further up. Now, let us explain activated. If there is an exception, and this is just a nor-
the macros in Figure 23. real EXIT from one of the blocks T,C1 ..... Cn in the try
The try(s) macro executes s and then throws the statement, this is then forgotten (set_this_EXN (N0_EXN)).
predefined EXIT object (exit_to_final). The EXIT ex- If on the other hand (else) it concerns an exception
ception is then caught by the finally macro (always in- that has not been caught, we need to remember it so
serted at the end) as we shall see. The catch (exn_E, x, s) that it can be re-thrown after the code in the finally
macro tests whether the current value of the EXN variable construct has been executed. We also need to make sure
satisfies the exn_E predicate (catch_cond (exn_E, x)), in that it does not activate unless constructs higher up
which case that branch is executed. during the execution of the finally code. One way to
The catch_cond (exn_E, e) macro in an atomic move do this is to negate it since the unless constructs in the
tests the predicate exn_E (hence is only executable when translation only react on positive values of EXN. When
it is true, see Figure 20 for one such predicate), and then we then leave the finally construct, we negate it back
stores the value of the exception in the local variable e to to its positive value such that it can be "thrown" fi_r-
 #define return_with(e)
#define Buffer_get_code(obj)
{ RES[TOP] = e;
throw(RETURN)
return_with(Buffer_get_x);
} #define return_without
unless {return_cond} throw(RETURN)

Fig. 24. qYanslation

ofthevaluereturning
get method #define return_cond
d_step{
get_this_EXN == RETURN ->
ther up. Some of the macros contain skip statements. set_this_EXN(NO_EXN)
These are necessary in order to make it work due to the }
semantics of the unless construct. Fig.25.Oper_ions_rreturnexceptions
In Figures 15 and 16 the macros a_finally(s) and
d_finally(s) are called. These are defined as respec- #define MAX_RESULT 5
tively atomic{finally(s) } and d_step{finally(s) }.
The d_finally(Buffermnlock(obj)) call in Fig- proctype Consumer_Thread(ObjRef obj){
ure 16 unlocks the object in case an exception has been
thrown out of a synchronized method. The d_step en- int RES[MAX_RESULT];
sures that the exception is not thrown further up during byte TOP;
the unlocking (which is more economic than negating the
exception) and the unlocking can be made completely Buffer get(Consumer get buffer(obj));
Consumer_run_received[Consumer_run_count] =
atomic since there-are no blocking statements.
RES [TOP];
The a_finally(Buffer_lock(obj)) call in Figure
15 locks an object after a call of wait has been inter- }
rupted. This locking must be as atomic as possible, but
Fig.26.The Consumerthread
with the possibility of blocking since another thread may
own the lock. Therefore a d_step cannot be used (it does
not allow blocking).
side effects. Consider for example the following state-
ment in the Consumer class's run method:
3.6 Value Returning Methods
received[count] = (AttrData)buffer.get() ;
A JAVA return statement can have one of two forms.
Ignoring the casting "(AttrData)...", the right hand
Either it has the form "return" in case the method is
side of this assignment has side effects, whereas the right
not value returning, or the form "return exp" if the
hand side of a PROMELA assignment does not allow this.
method is value returning. In either case, such a return
Our solution is to execute the method before the assign-
statement has the same effect as throwing an exception
ment, and then store the result value in a result array
that is caught by a "return exception handler" surround-
that is introduced for this purpose. Note that it has to
ing the body of the value returning method, and by any
be an array in order to model assignment statements of
finally constructs on the "way up" to that. Figure 24
the form "x = o.m(x) + p.n(y)" where several value
shows how the get method of the Buffer cla_s translates
returning method calls occur in an expression. Part of
with respect to value return. the translation of the Consumer class's run method is
We see that the body of the method is surrounded
shown in Figure 26. The Buffer_get macro will execute
by an unless construct triggered by the return_cond
and finally store the return value in RES[TOP], where
predicate. This predicate, defined in Figure 25, becomes
RES is the result array. This value is then "picked up" in
executable when the EXN variable in the executing thread
the assignment statement. Note that if there are several
(the one that executes the value returning method) gets
value returning method calls in a single expression, the
tlle value RETURN which is a predefined fixed object refer-
TOP variable is incremented for each during their eval-
ence. This happens for example when the return_with
uation, and then reset to its previous value before the
macro is called with an argument denoting the value re- values are accessed.
turned. The return_without models the return from a
method that does not return a value.
3.7 The main Method
The assignment "RES [TOP] = e" in the return_with
macro needs some explanation. The problem we are faced
with is that JAVA allows value denoting expressions to The main method of the Main class is translated into
contain calls of value returning methods that may have the PROMELA init section as can be seen in Figure 27.
side effects. In PROMELA expressions are of a syntacti- We have already explained the translation of object cre-
cally different class than statements, and cannot have ation, which is the only activity of this particular main
init{ The last two columns show the result of running the
{0bjRef Main_main_b; modified JAVA program on two versions of the JAVA Vir-
0bjRef Main_main_p; tual Machine (JvM) in order to see whether plainly ex-
0bjRef Main_main_c; ecuting the program would highlight the errors seeded.
atomic{
JVM version 1.1.3 is an older version being very deter-
0bjRef obj = create_object(Main,Main_Next);
ministic. This means that executing a multi-threaded
Main_Next++};
atomic{ program several times typically yields the same result

Main_main_b = every time. JvM 1.1.6 is the newer version with na-
create_object(Buffer,Buffer_Next); tive threads, where JAVA threads are mapped to Solaris
Buffer_Next++}; threads. This version is therefore non-deterministic, po-
Buffer_constr(Main_main_b); tentially yielding different results for different runs of a
atomic{ multi-threaded program.
Main_main_p = Every program has been run several times (from 30
create object(Producer,Producer_Next); to 100), and the numbers indicate the percentage of runs
Producer_Next++);
that have highlighted the error, either via a deadlock, an
Producer_constr(Main_main_p,Main_main_b);
assertion violation, or a thrown NullPointerException.
atomic{
All runs, model ctiecking as well as JvM runs, have
Main_main_c =
been executed on a Sun Ultra Spare 60 with 512 Mb
create_object(Consumer,Consumer_Next);
Consumer_Next++}; of main memory, and with the Solaris operating system
Consumer_constr(Main_main_c,Main_main_b); version 5.5.1.
} unless {get_this_EXN > 0} Running the SPIN model checker Oil the PROMELA
} code generated by JPF typically used less than half a
Fig. 27. The main method second to find an error and explored between 40 and 400
states and a similar number of transitions. In a few cases

(error S and 10) approximately 10000 states and 18000

transitions were explored in less than 2 seconds. The
method. Recall that the constructors of the Producer
memory consumption was around 17 Mb. This amount
and Consumer classes in this present example start the
of memory must probably be explained by the modeling
processes.
of the JAVA Virtual Machine within PROMELA.
"Errors" 11 and 20 are special (marked with a *)
in the sense that they are not really errors when us-
4 Analyzing the Program
ing the environment described in Section 2.2. This en-
vironment only creates one consumer, and to make the
The presented program is correct in the sense that no errors manifest themselves, we needed to create two con-
errors are found by SPIN when applied to the PROMELA sumers. In addition, with two consumers the assertions
code generated by JPF. In order to illustrate the effec- make no sense and were deleted. Hence, we were now
tiveness of JPF (and SPIN of course) we have seeded 21 just looking for deadlocks. The table rows for these er-
errors in the program shown in Figure 2, and for each er- rors show the result of verifying and executing in this
ror analyzed the now incorrect program using JPF. This changed multi consumer environment. The verification
experiment is described in the following. of error 11 needed as much as 8 minutes and 77 Mb,
exploring 2.4 million states and 6 million transitions be-
4.1 The Result
fore the deadlock was found. We verified a down scaled
version of this error, with a buffer size of 2 (instead of 3)
The results of this experiment are shown in Table 1.
and the producer only producing 3 values (instead of 6).
Also here the deadlock was found by the model checker,
For each error we give the line numbers changed, refer-
but now using 1 minute, 28 Mb, and exploring 423096
ring to Figure 2, and the new contents of these lines.
states and 1 million transitions.
As an example, error 1 is obtained by changing line 3
SPIN used 5.2 seconds to verify that the original pro-
to "protected int putPtr = 1;" (initializing to 1 in-
stead of to 0).
gram contained no errors. This involved the exploration
of 336S3 states and 61944 transitions, and a memory
The results of applying JPF are sho_na in the fourth
consumption of 18.8 Mb.
column. That is, the result of applying the SPIN model
checker to the PROMELA code generated by Jpr. The
possible outcomes are deadlock (D) and any of the two _.2 Comments on the Result

assertions being violated (A1 referring to the first oc-

curring "count == 6" and A2 referring to the second The example is small since its main purpose has been

"received[i] .attr == ±"). The point here is that all to illustrate the translation done by JPF. However, the

the errors are caught. exercise does show that around half (11) of the errors
 Table1.Verification
results
Nr. Line Modification
(changed
to) JPF JVM1.1.6 JVM1.1.3
1 3 protectedint putPtr= 1; A2 100 100

2 5 protectedint usedSlots= 1; A1,A2 100 100

3 9 while (usedSlots!= 3) D 100 100

4 9 while (usedSlots == 2) D 65 0

5 12 putPtr = (putPtr + 1) Y, 3; A2 100 100

13 array[putPrt] = x;

6 13 putPtr -- putPtr Y. 3; A2 100 100

7 13 putPtr = (putPtr + 1) Y. 2; A2 56 0
28 getPtr = (getPtr + 1) Y. 2;

8 14 if (usedSlots == 3) notifyAll(); D 33 100

9 14 remove: D 55 100
if (usedSlots == 0) notifyAUO;

10 14 usedSlots++ ; D 35 100
15 if (usedSlots == 0) notifyAll();

I]" 14 if (usedSlots == 0) notify(); D 2 100

29 if (usedSlots == 3) notify();

12 20 while (usedSlots == 0) D 100 100

13 23 if (usedSlots [= 0) { AI, D i00 I00

14 23 if (halted) { A1 3 0

15 29 if (usedSlots == 0) notifyAll(); D 50 0

16 29 remove: D 44 0
(if usedSlots == 3} notifyAllO;

17 29 usedSlots-- ; D 66 0
30 if (usedSlots == 3) notifyAll();

18 30 usedSlots++ A1, A2 100 100

19 35 remove: D 100 100

halted = true;

20" 36 notify() ; D 2 100

21 36 remove: D 100 100

notifyAll();
 consumer gets tile value in position 0, etc. The consumer
only gets the first three values. The producer then fin-
ishes and sets the halted flag, where after the consumer
Cou_ Nad-: 2 now gets an exception when trying to get the fourth
2--7 value (in position 0). Therefore the consumer will miss
l three values, and the first assertion (count == 6) will
be broken. Note that the second assertion is not broken.
Adding these print statements requires thought and
_g f_
work, but the idea may in fact be useful to cut down the
enormous amount of information contained in the error
traces created by SPIN.

5 Conclusion and Future Work

Fig. 28. Trace for error 14

In this paper we have described the initial prototype of
a translator from a non-trivial subset of the general pur-
are not guaranteed to be caught when plainly execut- pose programming language JAVA to the model checking
ing the program on the newest version of JVM, while in language PROMELA. We have also applied the transla-
contrast JPF finds the errors each time if present in the tor to 21 bugged variations of a small example program,
setup (errors 11 and 20 were not present with only one observing that tile model checker catches all tile bugs,
while executing the programs only catch the bugs safely
consumer). The difference is most obvious for errors 11,
in half of the cases.
14 and 20. Errors 3 and 11 were suggested by a reviewer.
The chance of catching errors by executing the program: " _,Ve are currently applying the translator to a collec-
gets even smaller when the program size increases.• tion of reM programs developed within NASA, and the
outcome of these experiments will be published at a later

.3 Error- Traces - time. As an example, a collaboration with NASA's God-

• _ dard Space Center involves the verification of a satellite
When SPIN identifies an error in the translated PRO_,_ELA file down-link protocol written in JAVA. The translator
has in addition been applied to analyze a Chinese Chess
. 'code, be it a deadlock or an assertion violation, it rbturns"
game server application written in JAVA. This lead to
r with an error trace showing the sequence of executed
the confirmation of a suspected deadlock and the iden-
PROMELA statements leading from the initial state to
tification of a smaller scenario leading to that deadlock.
the state where the error occurs. Our tool does not cur-
This work is documented in [13].
" rently map such PROMELA error traces back to corre-
Although the translator covers a non-trivial subset
sponding JAVA traces. As an alternative, we have ex-
i of JAVA some important features are not covered. These
tended tile Verify class with special print methods
are: packages, overloading, method overriding, recursion,
which can be called (by the programmer) in selected
strings, floating point numbers, static variables and meth-
places in the JAVA code. These calls will then be trans-
ods, some thread operations like suspend and resume,
lated into PROMELA print statements set up to print
some control constructs, such as the continue state-
on a graphical two dimensional message sequence chart.
ment, and garbage collection. In addition, arrays are
Figure 28 shows such a chart illustrating the trace for
not objects as they are in JAVA. We model arrays us-
error number 14.
ing PROMELA'S own arrays to obtain efficient verifica-
To obtain this chart, to be explained below, we have
tion. The current implementation thus does not allow
added print statements 5 places in the code. For exam-
arrays to be first class values and they cannot be nmlti-
ple, in lines 12 and 26 (pushing current lines downwards)
dimensional. Finally, we do not translate the predefined
we have added the statements:
class library. Some of these features are hard to trans-
12 Yerify.print("put",putPtr) ; late, such as recursion, strings, floating point numbers,
26 Verify.print("get",getPtr) ; and garbage collection. The rest are relatively straight
Hence, what will be printed out is a text string ("put" forward, although an efficient translation of dynamic ar-
or "get"), and the position in the buffer where a value rays as objects is not evident. We continue to extend the
is stored (put), respectively retrieved from (get). Other translator to cover more of JAVA.
print statements record other events, such as the pro- An essential question is whether the translation is
: ducer setting the halted flag, and the consumer getting optimal. We still need to evaluate this question. There
- the corresponding exception. Figure 28 illustrates a situ- may be other ways to translate into PROMELA and one
- ation where the producer (center vertical line) first pro- may consider making a by-pass, avoiding PROMELA, and
- duces two values, stored in positions 0 and 1. Then the translating directly into the C interface to the SPIN model
checker. A major point of discussion has been how to Penix and Willem Visser for proof reading the manuscript.
We also thank the reviewers. We have used a Java parser
model object creation. One obvious solution would be
to use PROMELA'S proctypes to model classes, and then ported by Peter Sestoft (the Royal Veterinary and Agricul-
tural University in Denmark) to Moscow ML from a Standard
spawn a process for each object creation. This would in-
ML version written by Olivier Brunet and Gordon Wood-
deed help at the level of memory allocation and result in
hull in Alex Aiken's group (University of California, Berkeley,
a simpler translation than into arrays. However, it con-
USA).
flicts with the fact that several threads can access the
same object concurrently: a PROMELA process only has
one thread of control.
References
Recently JPF has been modified to translate object
synchronizations and exceptions more efficiently by in-
troducing two new special purpose arrays holding lock- 1. K. Arnold and J. Gosling. The Java Programming Lan-

ing and exception variables, thus keeping these variables guage. Addison Wesley, 1996.
R. Iosif C. Demartini and R. Sisto. Modeling and Vali-
separate from user defined variables. This gave a 50% 2.
dation of Java Multithreading Applications using SPIN.
reduction in the amount of C-code generated by SPIN.
In Proceedings of the 4th SPIN workshop, Paris, France,
We have presented the simpler solution for readability November 1998.
reasons. 3. T. Cattel. Modeling and Verification of sC++ Applica-
We see the current translator as a phase 1 proto- tions. In Proceedings of the Tools and Algorithms ,for the
type experiment (involving 9 man months until now) Construction and Analysis o/Systems, Lisbon, Portugal,
that provides us with useful input to a phase 2, where LNCS 1384., April 1998.
these questions will be raised. What is equally impor- 4. J. C. Corbett. Constructing Compact Models of Concur-
tant is our planned efforts to build an abstraction work- rent Java Programs. In Proceedings o/ the ACM Sigsoft
bench around JAVA, where programs can be reduced in Symposium on So/tware Testing and Analysis, Clearnva-
size before model checking is applied. Techniques such ter Beach, Florida., March 1998.
D. L. Delefs, K. R. M. Leino, G. Nelson, and J. B.
as program slicing, abstract interpretation, and partial 5.
Saxe. Extended Static Checking. Technical Report 159,
evaluation will have a great influence.
Compaq Systems Research Center, Palo Alto, California,
We believe that the kind of technology presented in
USA, 1998.
this paper, already as is, can be very useful for unit test-
J. Gosling, B. Joy, and G. Steele. The Java Language
ing where one focuses on a single or a few classes, just 6.
Specification. Addison Wesley, 1996.
as has demonstrated with the example. This requires 7. K. Havelund. Mechanical Verification of a Garbage Col-
setting up an aggressive environment consisting of a col- lector. In Fourth International Workshop on Formal
lection of threads which will "bombard" the unit with Methods for Parallel Programming : Theory and Appli-
accesses. The technology is probably ready for this al- cations (FMPPTA '99), Lecture Notes in Computer Sci-
ready now, since there will typically not be a big need to ence, April 1999. To appear.
cut down the state space. Finally, we believe that per- 8. K. Havelund, K. G. Larsen, and A. Skou. Formal Ver-

haps the technology can be useful for students learning ification of an Audio/Video Power Controller using the
Real-Time Model Checker UPPAAL. In 5th Int. AMAST
to program in JAVA.
Workshop on Real-Time and Probabilistic Systems, Lec-
Concerning the specification language, our main ap-
ture Notes in Computer Science, May 1999. To appear.
proach has been not to extend the JAVA language but to
9. K. Havelund, M. Lowry, and J. Penix. Formal Analysis
express temporal properties as calls to methods defined of a Space Craft Controller using SPIN. In Proceedings o/
in a special temporal logic class (the Verify class), all of the 4th SPIN workshop, Paris, France, November 1998.
whose methods are static (hence one does not need to in- 10. K. Havelund and T. Pressburger. Translating Java to
stantiate the class to objects before calling the methods). SPIN, a step towards the JavaProver. Technical report,
In addition to the assert method one can for example NASA Ames Research center, Moffett Field, California,
imagine an always method, an eventually method, and USA, May 1997.
basically include all of SPIN's linear temporal logic op- 11. K. Havelund and N. Shankar. Experiments in Theorem

erators as methods, having boolean return types in ad- Proving and Model Checking for Protocol Verification.
In M-C. Gaudel and J. Woodcock, editors, FME'96: In-
dition to boolean argument types, such that they can be
dustrial Benefit and Advances in Formal Methods, vol-
composed. Calls of such methods will then generate LTL
ume 1051 of Lecture Notes in Computer Science, pages
formulae to be verified, referring to the position where
662 681, 1996.
they are called in the code. K. Havelund and N. Shankar. A Mechanized Refinement
12.
Proof for a Garbage Collector. Submitted to the journal:
Acknowledgements. We thank Gerard Holzmann for chang- Formal Aspects of Computing, 1998.
ing SPIN to support the translation of exceptions. We thank 13. K. Havelund and J. Skakkeb_ek. Practical Application
the members of the Automated Software Engineering team of Model Checking in Software Verification. Describes
at NASA Ames Research Center for their comments; and in an application of JPF to a game server. Submitted for
particular Mike Lowry for supporting the project, and John publication., February 1999.
14.K. Havelund,
A. Skou,
K. G.Larsen,
andK. Lund.For-
malModeling
andAnalysisofanAudio/Video
Protocol:
AnIndustrialCase
StudyUsingUPPAAL.In Proc. of
the 18th IEEE Real-Time Systems Symposium, pages 2-
13, Dec 1997. San Francisco, California, USA.
15. G. Holzmann. The Design and Validation of Computer
Protocols. Prentice Hall, 1991.
16. D. Lea. Concurrent Programming in Java. Addison Wes-
ley, 1997.
17. B. PelI, E. Gat, R. Keesing, N. Muscettola, and B. Smith.
Plan Execution for Autonomous Spacecrafts. In Pro-
ceedings of the 1997 International Joint Conference on
Artificial Intelligence, 1997.