SystemC to Timed Automata Transformation Engine (STATE)
STATE takes a SystemC design as input and transforms it into a corresponding UPPAAL timed automata model. The transformation is based on a formal semantics defined for SystemC in [Her08],[Her10],[Her11],[Pockr11],[Pockr13],[Her13]. The general idea is to map the informally defined semantics of SystemC to the formally well-defined semantics of UPPAAL timed automata. This mapping defines a formal semantics for SystemC, and, at the same time, it enables the automatic transformation from a given SystemC design into a semantically equivalent UPPAAL timed automata model. The transformation preserves the informally defined semantics of SystemC completely. To ease debugging, it also keeps the structure of the original SystemC design transparent to the designer in the UPPAAL model (through prefixing). The current version of STATE supports structs, pointers, and arrays as well as the TLM 2.0 standard.
STATE is licenced under GPL and freely available. The examples described below are included in the zip file provided in the download section.