SymRTSymbolic Execution and Model Checking for Timing Analysis of Real-Time Java
What is SymRT?
SymRT is a timing analysis tool for real-time Java systems written in a variant of the Safety Critical Java profile. It combines symbolic execution using Symbolic PathFinder with model checking using UPPAAL; the former is used for extracting the feasible execution paths of the system while the latter is used for conducting the actual analysis by viewing them as reachability model checking problems. SymRT can build two different timing models;
- A complete timing model, which includes the scheduler and the actual real-time task releases (periodic or sporadic) as well as a model of the execution environment. This model is rich enough for conducting schedulability analysis, WCET, BCET, Worst Case Blocking Time, and processor utilisation and idle time analysis.
- A WCET and BCET optimized timing model which includes only the execution paths (and thus the temporal behavior) of the target method.
SymRT uses jpf-symbc-rt, an extension project to Symbolic PathFinder, which performs the symbolic execution and generates the Timed Automata. Jpf-symbc-rt was developed as part of SymRT and can be used standalone. The project website for jpf-symbc-rt can be found on bitbucket HERE.
Obtaining SymRT
You can try SymRT by either downloading the pre-compiled runnable jar or by downloading the source code and compile it yourself. The pre-compiled version, also includes execution environment models that can be used for evaluating SymRT. There is currently support for HVM on AVR, and JOP.
A package containing the UPPAAL models used in the evaluation section in the paper can be found HERE. The source code for the Mälardalen WCET benchmarks used in the evaluation including the JPF configuration files for producing the models can be obtained HERE. These are slightly modified versions of the original Mälardalen WCET benchmarks implemented in Java which can be found in the JOP distribution.
Using SymRT
SymRT is a command-line tool and is configured through a number of command line arguments. All configurations can be found using:
> symrt.jar --help
Assuming you want to generate a WCET/BCET optimized model you could use:
> symrt.jar --classpath "project/bin" -symbc -spfcp "jpf-symbc classpath here" -optwcet "package.clazz.comp(sym#sym)" package.clazzThis will generate a WCET/BCET optimized timing model for the comp method with two symbolic inputs
If you want to make a complete timing model, this can be done using e.g.:
> symrt.jar --classpath "project/bin:scj2_v1.jar" -symbc -spfcp "jpf-symbc classpath here" --platform jop -wcet -wcrt package.clazzThis generates a complete JOP timing model for the real-time system with entry point in class clazz i.e. it contains the main method where all real-time task instantiations are performed. The timing model furthermore facilitates WCET and WCRT analysis to be conducted.
Requirements
SymRT 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.