04 Apr 10 Java Path Finder

The Java Path Finder is an open source project developed by the people at Nasa Ames research center dedicated to verification of software. The focus is on formal methods and other related automated/semi-automated verification techniques. I have been learning about this topic and related topics like logic and automata theory during my Masters in Chennai Mathematical Institute. My home page is here. Currently, I am working on my thesis on “Topics in Logic and Automata theory”.

Getting Started with jpf

The jpf project only verifies Java software. It has a really unique way of doing this, by taking the java classes and running them over the actual JVM. It acts as an intermediary between the System Under Test(SUT) and the actual JVM as illustrated here. It is well known that in general, the Model Checking problem is really hard, in terms of both space and time and hence in practical verification tools, there is always a trade-off between complete model checking and efficiency in terms of time and space. Let me not get into that for the moment (at least not in this post) as it is a really vast topic and a field of intense research.

However, what I will talk/rant about in this and the next few posts is how to get the jpf system up and running. This is one of the reasons that I am not a great fan of java, c or c++ as there is such a steep curve in getting things installed or built or configured.

There are many ways of obtaining and installing jpf and it can get very confusing. First of all you need to have mercurial installed on your system, as, the version control system used by the jpf team is mercurial. Thus, using apt-get, we can install mercurial on Ubuntu as follows

sudo apt-get install mercurial

Obtaining the Software

Now, you have the following two options to obtain the jpf software (source code/ binaries):

1. Either get the binary snapshot as explained here .
2. Or obtain the source code from the jpf repositories as described here.

Getting the binaries is pretty straightforward. All you need to do is download the zipped file and it does not need mercurial. The binaries, however, are a bit stale and do not reflect the current updates made to the jpf system. Hence we might need to obtain the source code which may be procured in any one of the following three ways :

1. From the command line
2. Using the NetBeans IDE
3. Using the Eclipse IDE

My Reviews and Experiences

All above three methods require that you have mercurial installed. If you have Ubuntu or a debian-based distro, you can get mercurial by using sudo as I just explained above. However, after getting mercurial installed I had a pretty tough time with obtaining jpf on eclipse. On NetBeans it was very easy to obtain the jpf source code but I was not able to verify/run jpf on any example programs. The command line option was the easiest and most hassle-free option to obtain, build and run on example programs. Hence that is the route that I would recommend any newbie take initially.

Next post I intend to explain on how to obtain, build, install and verify an example application/program using jpf.