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;

SymRT is flexible to accommodate the execution environment of the analyzed system into the analysis, which is a result of translating the symbolic execution tree characterizing the feasible paths to the Network of Timed Automata formalism of the UPPAAL model checker; the constituents of the analyzed systems are logically grouped into NTA Layers; Program NTA, JVM NTA, and Hardware NTA and their parallel composition yields the complete model.

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.clazz
This 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.clazz
This 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.

Kasper Søe Luckow, Corina S. Pasareanu, and Bent Thomsen.