SystemC To Timed Automata Transformation Engine (STATE)
-------------------------------------------------------

STATE is a SystemC to Timed Automata Transformation Engine. It takes a
SystemC design and transforms it into a corresponding UPPAAL timed
automata model.

The input of STATE is the Abstract Syntax Tree (AST) of a SystemC
design as generated by the Karlsruhe SystemC Parser (KaSCPar),
provided by the Karlsruhe Forschungszentrum Informatik (FZI). KaSCPar
is licensed under GPL. We provide a slightly adapted version of the
KaSCPar tool SC2AST, which also accepts and processes TLM keywords at
http://www.pes.tu-berlin.de/state_project

Requirements
------------

Both KaSCPar and STATE are implemented in Java and should be
executable on most systems. However, we only tested them under Linux
12.04 (Precise Pangolin) and Windows 8.

Transformation
--------------

I. Using jar files directly:

To transform a given SystemC Design into Uppaal using STATE, do the following:

1. Generate the AST with KaSCPar:

java -jar sc2ast.jar -f source_file1 [.. source_fileN] -o kascpar_output_file

This will generate the file kascpar_output_file.ast.xml.

2. Transform the it with STATE:

java -jar sc2uppaal.jar -i kascpar_output_file.ast.xml -o state_output_file.uppaal.xml

This will generate the file state_output_file.uppaal.xml, which can be opened and verified using the UPPAAL Model checker, available at http://uppaal.org/.

II. Using provided Makefiles

You can then transform all examples by typing

make uppaal

in the corresponding folder.


Examples
--------

We provide five examples with this distribution: a simple FIFO, a
simple ABS/ASR system, a blocking transport, a non-blocking transport,
and a TLM implementation of the AMBA Advanced High-perfomance Bus
(AHB). More details about these examples can be found at
http://www.pes.tu-berlin.de/state_project.

----------------------------------------------------------------------

For any problems or questions, please contact: state@pes.tu-berlin.de



