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.
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.
- Annotated source code of the analysed Java program (containing e.g. loop bounds).
- A compiled executable of the analysed Java program.
- A model of the JVM*
- A model of the execution environment*
*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.