Tautoko

About

Tautoko is a prototype implementation that mines enhanced specifications by mutating and running the regression test suite of a program.

Example Usage

To illustrate the usage of Tautoko, we have created a small example application that consists of a class called MyProtocol and a regression test suite MyProtocolTestSuite for this class:

1 package tautoko.examples;
2 
3 public class MyProtocol {
4 
5         public static final int ST_DEFAULT = 1;
6 
7         public static final int ST_CONNECTED = 2;
8 
9         public static final int ST_AUTHENTICATED = 3;
10 
11         private int state = ST_DEFAULT;
12 
13         public MyProtocol() {
14 
15         }
16 
17         public void connect() {
18                 if (state != ST_DEFAULT) {
19                         throw new IllegalStateException();
20                 }
21                 state = ST_CONNECTED;
22         }
23 
24         public void authenticate(String userName, String password) {
25                 if (state != ST_CONNECTED) {
26                         throw new IllegalStateException();
27                 }
28                 state = ST_AUTHENTICATED;
29         }
30 
31         public void quit() {
32                 state = ST_DEFAULT;
33         }
34 
35 }

MyProtocolTestSuite.java :

1 package tautoko.examples;
2 
3 public class MyProtocolTestSuite {
4 
5         private MyProtocol protocol;
6 
7         /**
8          * @param args
9          */
10         public static void main(String[] args) {
11                 MyProtocolTestSuite testSuite = new MyProtocolTestSuite();
12                 testSuite.setup();
13                 testSuite.testConnect();
14                 testSuite.testAuthenticate();
15                 testSuite.testQuit();
16         }
17 
18         public void setup() {
19                 protocol = new MyProtocol();
20         }
21 
22         public void testConnect()       {
23                 protocol.connect();
24         }
25 
26         public void testAuthenticate() {
27                 protocol.authenticate(null, null);
28         }
29 
30         public void testQuit() {
31                 protocol.quit();
32         }
33 }

These two classes are contained in the Tautoko package which is available for download at the download page. To run the example, you need to adhere to the following procedure:

Download and extract the Tautoko package from the download page. This should create a folder name tautoko-cli-0.1-SNAPSHOT.
Change to this folder. You should now be able to see four subfolders:
- bin holds two different bash scripts: runtautoko.sh invokes Tautoko, whereas runexample.sh calls runtautoko.sh to enhance models for the example application.
- examples contains the example files as listed above.
- lib contains all libraries required to run Tautoko.
- res contains the log4j configurator.
You need to make the scripts in folder examples/bin executable.
Change directory to folder examples and run bin/compile.sh to compile the example files.
Change directory back to tautoko-cli-0.1-SNAPSHOT.
Edit bin/runexample.sh and change the second line to point to a Java compiler executable (javac) . You should not need to edit anything else.
Run bin/runexample.sh . This should launch Tautoko. You will see a couple of debug messages that indicate the progress. Once Tautoko has finished, you will find the results in folder examples/results.

JFTA

About

JFTA is a partially interprocedural flow-insensitive typestate verifier for JAVA. JFTA takes as input a set of specifications in GraphML format and a program that is checked against the specifications. A detailed description of JFTA is available in this thesis. JFTA can be downloaded at the download page. An example specification can be downloaded here.

Running JFTA

In order to run JFTA, your system has to meet the follow requirements:

Unix based OS (MacOS 10.5 or Linux)
Java 1.6

In principal, JFTA should also run on Windows, however we never tested if it actually does. To execute JFTA, you have to do the following:

Download the binary version of JFTA here.

Unpack using unzip. You should now see folders lib and bin. Folder bin contains a bash script that assembles the class path and starts Java. Usage of JFTA is as follows:

        --help                                  prints this usage information and quits

 Parameters which MUST be specified at least ONCE:
        --classfiles               resource (folder/archive) containing bytecode of all classes
        --specfiles                     folder containing specification XML files

 Parameters which might be specified multiple times:
        --testclass                 qualified class name (package/package/Class) of ONE class of which all
                                                methods are to be analyzed
        --testmethod               qualified method name (package/package/Class.method(Ljava/lang/Object;)V)
                                                giving a method which is to be analyzed

 Option switches:
        --showNoSpecWarnings                    enables printing warnings about types without specification

        --oneWorklist                           uses only one worklist in the analysis algorithm

        --maxDepth  (default 1)            maximum level to which the call analysis descends

        --topPolicy                     sets how calls on TOP state types are handled.
             == everyState              assume object being in any possible state (except 'start' and 'ex')
             == firstOk (default)       assume that the first call on the object never produces an error

        --unknownTransition             sets how a transition, which is unknown to the object's
                                                specification, is handled (only if there is a spec. for this type)
             == ignore                  the object does not change its state
             == error (default)         the object performs a transition to the error state
             == report                  generate a distinct violation for unspecified transitions

        --loglevel                       sets the logging level
             == ALL, TRACE, DEBUG,       possible levels sorted by decreasing verbosity
                       INFO (default),          
                       WARN, ERROR, OFF