Next: Introduction
Up: A Concurency Analysis
Previous: A Concurency Analysis
Abstract:
This report describes the model of a formal description generator for Java
code. The translator tool produces as output a description of the Java source
in the form of a Promela script. This is used by the Spin analyzer to detect
potential deadlock situations. The output produced by Spin is used to locate
in the original Java code where such situations can occur, in order to provide
a real help to the developer. The generated formal description will ignore
parts of the original Java code which are not involved in thread communication.
Some generalization of a thread description has to be done in order to obtain
the corresponding Promela specification that reflects the behavior of the
thread. This can lead to false warnings, but will never cause real errors to be
ignored. The translation tool contains a front-end part and a back-end. The
front-end translates the source program into an intermediate representation
from which the back-end generates target code. Static checking is done on the
intermediate representation in order to detect semantic errors. The back-end of
the translator generates a Promela description according to the internal
representation builded by the front-end. It uses a template model to describe
thread communication via synchronized blocks and methods and monitor
mechanisms. Note that this project takes into consideration only
multi-threading communication systems. Streams, Sockets and Remote Procedure
Invocation are seen as part of the multiprocess communication, therefore, they
are not taken into consideration.
Radu Iosif
Thu Apr 9 15:10:10 MET DST 1998