About
This website is under construction.
Installation
These instructions are for installing TJT in Windows 7. Instructions for other compatible operating systems may be added in the future.
Requirements
You will need the following:
Installation guide
- Install Cygwin if you do not have it already installed. Make sure the following additional packages are installed: GCC, Bison, Flex and XDR RPC.
- Install Spin by placing the executable file somewhere in the Windows PATH.
- Install the FreeHEP Java XDR library by placing the JAR file in the \lib\ext directory of your JDK installation directory or, alternatively, in your Java CLASSPATH.
- Copy the plug-in JAR file into the \plugins directory of your Eclipse installation.
- Copy this files and unzip them into the root directory of your Eclipse installation. Usually C:\eclipse.
Tool guide
The first thing is to active the traces view, by clicking at Window/Show View/Other on the tool bar, and then selecting TJTPlugin/Traces.
If you want to use our tool, you need to have a compiled Java project in Eclipse. You have to create a special file by clicking with the right mouse button over the project folder. In the menu you have to select New/Other/TJT/TJT configuration file. In the next window you must select the project where you want to store that new file. If the file is opened with the default editor you must close it and always open it with our special editor. For that, right mouse button over the created XML file and select Open With/ TJT Configuration Editor.
Once you have opened the configuration with with the editor, you see several different parts divided in tabs. Note that some of them might not be explained but you have them in the configuration files (they are still in experimental process and only hash implementation is currently released). The most important tabs are explained next:
- General: Here we must introduce the name of the main class. If the class is in default package we just have to type the name of the class, otherwise, we have to type the complete path, separated by character '.'. For example, if my main class is 'MyMain' and it is in package 'Lists', we should type Lists.MyMain in the proper field (i.e. packages starting from the root until the main class separated with dots).
In combo projection we can choose the sort of projection (hashing or with an incremental counter).
Objective combo lets you to choose between:
- 'all'(all traces must satisfy the formula, usually for a desired behavior specification).
- 'any' (at least one trace must satisfy the formula).
- 'none' (all traces must not satisfy the formula, usually for a bad behavior specification).
Besides we can indicate the number of times we want to perform the verification in 'Repeat' field. If we do not modify this parameter (value=0) test will only performed one time. In 'Max inactivity' you can adjust how much time you set before TJT detects it.
- Property: Here we must write the formula, according to SPIN syntax. Below the formula text field, we have to define the different propositions. We can use the buttons Add and Remove for define or delete them. The column Name indicates the literal, and Expression is referred to the content of the proposition. We have to specify it as a C language condition. If there are variables involved in the definition, we have to write them like in Java, i.e. the name of the path separated by character '.' and finally the name of the field. Besides the current program variables, we can define propositions over a special variable, i.e. 'location', that represents the location of the program at the last monitored point. That special variable is modified when a monitored variable is changed, when an exception is thrown and when a breakpoint is detected. Note that the formula you write is introduced inside a never claim, so if the property accomplishes, this trace is erroneous. Otherwise you can negate your initial formula in order to detect the traces that does not satisfies it.
- Variables: In this tab, we can choose which mode of monitorization we want. 'Modification' will send us changes produced at the moment the happen, 'Method' will send us changes at the end of the method where it happen (In the case of some marked variables were changed, the tool would send us only one new state).
But the best part of this tab is the table with all the fields of the project. We can mark the fields we want for monitorization and use them inside the properties. If we mark 'As Object' and a numeric value indicating the maximum number of instances, we will have in our SPIN state vector one variable for each possible instance. Otherwise we will have one field, that will be modified for several instances (if there are).
- Locations: In some case, we could want to check if some location of the code is reached over some scenario. In our tool, we can add breakpoints, that will be indicated by JDI to SPIN. In the column Source we have to write the name of the class in the same way above mentioned (full name). In Line we have to write the number of line.
- Safe locations: Here we are able to set location where the application may block in a safe way (not a deadlock). We add them in the same way that current locations explaine above.
- Java asserts: As that tool is for Java, we can set asserts to prune a trace if it does not satisfy them. Once we press 'Add' button, in first column we set the variable implied, in second the operator and in the last the desired value.
- Arguments: If our application needs arguments in the main method, we can add them in this tab. In column Values we can specify ('separated by comma'), the different values for the same argument position. Later, SPIN will perform each possible combination between the arguments.
- Operations: Here we have 'Launch' button, that executes the test. Make sure you save the changes on the configuration file and build the Java project before launching. At the end of it we will be notified. Once a test has finished, we will see at the Traces View if erroneous executions happened. Watching on TJT console the information that appears may be very useful too. It will probably automatically show up with information in the current Eclipse console area, otherwise select 'TJT' in Console Selection button of your Eclipse panel.
Once we have performed a test with our tool, we will see how the Traces View changes (otherwise try pressing the rescan button of the view), and an item with the project name is added. Depending on the result of the test, we can expand that item and see the different(s) execution(s) trace(s). When we click over a determinate location, we will see the class it belongs and the concrete line remarked in a new window. Following the course of the execution, we can extract conclusions about the behavior of our code and why errors appeared. Besides erroneous traces information you are able to see in real time what is happening during the execution by selecting TJT console in Eclipse console view. A trace file by itself contains useful information, because it stores in order the operations performed in the tested Java program to that concrete trace. We also are able to watch the values of the variables in a proper view.
Examples
We provide you the code we have tested. Note that this codes have been slightly modified for performing easily and automatically the different tests. This modification is neccesary only with servers and programs with an infinite execution to save time and to have a stop condition in some cases.
To use anyone of them you must create an Eclipse project, and import the packaged file to it. Each package also contains the configuration files for evaluating the properties we tested in its root directory. Make sure you build the project before launching the test. We recommend you to test first the configuration files as they are, and later try changing some parameters.
To use our tool, you may open the concrete test file by clicking Open With/TJT Configuration Editor. Then you have to proceed as explained in the tool guide.
FTPD
Download this example project
This code consists of a complete FTP Java server, with an additional part added by us that simulates the behavior of a client according to our purpose.
Java NFS server
Download this example project
This code contains a NFS server with an internal client which performs operations against the server.
WebServerLite
Download this example project
It is a code for a http server. As the others servers above exposed, this one contains a small additional code that simulates the behavior of client.
Elevators
Download this example project
Download this example project
This is a concurrent program, with one elevator and several users that try to access it. The first link is a good implementation and the second is wrong implemented in order to see the errors.
Lists management
Download this example project
This program contains performs operations in lists inside a cycle.
Random numbers
Download this example project
This project contains three different classes that performs method accesses according to random numbers results. They are used as examples in jpf-ltl too.
