TetaJ Tool for Execution Time Analysis of Java bytecode

What is TetaJ?

TetaJ is tool that can be used for determining execution times of Java bytecode based programming languages executed on a Java Virtual Machine running on arbitrary processors. The fundamental technique is to transform the program and implementation of the JVM into timed automata together with a model of the behaviour of the processor. UPPAAL is used as model checker to determine the WCET of the program. Currently, TetaJ offers explicit support for Hardware near Virtual Machine (HVM) and the AVR family of processors from Atmel. Specifically, the ATmega2560 processor has been used during the development of TetaJ.

Download TetaJ

To try TetaJ you can either download the compiled version or download the source code and compile it yourself.

Using TetaJ

TetaJ consists of three tools: the model generator tool, the model combiner tool, and the model processor tool.

In order to estimate the WCET of a given Java method, the following must be provided to these tools.

*models for the execution environment used in our case study are provided in the binary download.

> java -jar ModelGenerator bin/ javaClass#main()V src/ jbcmodel.xml
> java -jar ModelCombiner jbcmodel.xml jvmmodel.xml staticjvmmodel.xml hardwaremodel.xml -o combined.xml
> java -jar ModelProcessor combined.xml


Currently, TetaJ has been tested on Ubuntu 10.10 and Gentoo Linux, so following will presume either of these.

The model checker tool UPPAAL is required, specifically, its verification engine tool verifyta must be located in your PATH environment variable.


Christian Frost, Casper Svenning Jensen, and Kasper Søe Luckow,
Department of Computer Science, Aalborg University, Denmark.