Transforming SystemC Transaction Level Models into UPPAAL timed automata

The SystemC Transaction Level Modeling (TLM) standard is widely used for modeling and simulation in hardware/software co-design. However, the semantics of the TLM core interfaces is only informally defined. This makes it impossible to apply formal verification techniques to transaction level models that conform to the TLM standard. To solve this problem, we propose a formal semantics of the TLM transport mechanisms using timed automata. We achieve this by providing a set of timed automata templates that precisely capture the semantics of the TLM core interfaces. Then, we use this set to transform a given SystemC-TLM model into a semantically equivalent timed automata model. The transformation is an extension of our previously proposed transformation from SystemC into Uppaal timed automata and can be used to verify safety, liveness, and timing properties of TLM models using the Uppaal model checker. We demonstrate the applicability and performance of our approach with two case studies, namely a loosely-timed model that uses a blocking transport and an approximately-timed model that uses a 4-phase non-blocking transport.