TetaSARTSA Flexible Schedulability Analysis Tool for SCJ Programs

What is TetaSARTS?

TetaSARTS is a fully automated tool for conducting schedulability analysis of Java Bytecode systems. It also allows incorporating the execution environment in the analysis which may either consist of a hardware implementation of the JVM, such as JOP, or a traditional software implementation running on embedded hardware. TetaSARTS was conceived with the purpose of being flexible and accommodate virtually all configurations of the execution environment and scheduling policy employed in the analysed system. It achieves this goal by adopting a model-based technique where the entire analysed system is translated to the Networks of Timed Automata (NTA) modeling formalism of the state-of-the-art UPPAAL model checker. The NTA is generated such that it architecturally resembles the original structure of a Java Bytecode system in layers. Each layer can be substituted, hence making it possible to easily switch the analysis to incorporate e.g. other execution environments.

Obtaining TetaSARTS

You can try TetaSARTS by either downloading the pre-compiled distribution or by downloading the source code and compile it yourself. The pre-compiled version, also includes models that can be used for evaluating TetaSARTS. There is currently support for HVM on AVR, and JOP

Another option is to download the VirtualBox Ubuntu 12.10 image which includes the TetaSARTS executable and the experiments used. The image also includes a description of how to run the experiments using the provided scripts. You do, however, need to download the UPPAAL verification engine, and put it in your PATH. The image can be downloaded HERE.

Using TetaSARTS

An example of using TetaSARTS:

> TetaSARTS.jar -m --main-entry-point main --scheduler fps --devirtualization-analysis vta -o /outputpath/ experiments.SimpleRTS

This generates an NTA for the SimpleRTS system with an FPS scheduler and with a JOP execution environment. Virtual method calls are resolved using variable type analysis. TetaSARTS also features a wide variety of other options which can be shown by consulting the help/usage menu:

> TetaSARTS.jar --help

Requirements

TetaSARTS has been tested on Ubuntu 12.12 and Gentoo Linux. Besides the distribution, the UPPAAL verification engine is also required which can be obtained at: UPPAAL.

Contact

• Kasper Søe Luckow (luckow@cs.aau.dk)
• Thomas Bøgholm (boegholm@cs.aau.dk)
• Bent Thomsen (bt@cs.aau.dk)