hiJaC Tools
The hiJaC Tools are openly available here.
The model translator produces Circus models from SCJ programs.To use the model translator on the cruise controller example, as reported in our paper submitted to The Computer Journal, please first use "ant" within the trunk folder to compile the source code and then execute the "run" script. The tools are currently only tested under Linux. Please see the README.txt file in trunk for further instructions.
If any problems with the tool please feel free to get in touch via email with Frank Zeyda.
TransMSafe
The TransMSafe tool is used to check for possible memory-safety violations inside Level 1 SCJ programs. Given a valid SCJ program according to the SCJ specification, the tool uses static analysis to identify statements that may break the memory-safety rules of SCJ. More specifically, if a statement changes a reference to point to an object that may reside in a memory area lower in the memory hierarchy, an error is raised.
To achieve this, the tool keeps a record of the necessary aliasing and reference information in a bespoke environment. A worst-case model of the program is stored in the environment, which is maintained and analysed throughout the program analysis. A more in-depth description of the technique employed by the TransMSafe tool can be found in the publication SCJ: Memory-Safety Checking without Annotations.
The tool can be downloaded here. The tool is based on the infrastructure defined in the hiJaC tool suite, which offers other facilities for SCJ such as the Circus model generator for SCJ.
The source code for the TransMSafe tool can be found in the src\java\hijac\tools\scjmsafe directory. Instructions on how to build and run the tool with the provided examples can be found in the README file in the root directory.
TightRope
TightRope is a tool for automatically modelling SCJ Level 2 programs by translating them into Circus. It is a substantial extension of the original Model Translator provided above, although it reuses the infrastructure and some functionality from the Model Translator.
The output from TightRope differs greatly from that of the Model Translator. This is because we address the features of Level 2 and extend the Model Translators coverage of Level 1 by capturing: period and deadline overruns, exceptions, and synchronisation. TightRope requires that the input program compiles and that each class is in a separate file. The prototype version of TightRope (v0.65) is available here. The archive contains a readme with instructions on how to run TightRope on the two example applications included