Model checking SystemC designs using timed automata

SystemC is widely used for modeling and simulation in hardware/software co-design. Due to the lack of a complete formal semantics, it is not possible to verify SystemC designs. In this paper, we present an approach to overcome this problem by defining the semantics of SystemC by a mapping from SystemC designs into the well-defined semantics of Uppaal timed automata. The informally defined behavior and the structure of SystemC designs are completely preserved in the generated Uppaal models. The resulting Uppaal models allow us to use the Uppaal model checker and the Uppaal tool suite, including simulation and visualization tools. The model checker can be used to verify important properties such as liveness, deadlock freedom or compliance with timing constraints. We have implemented the presented transformation, applied it to two examples and verified liveness, safety and timing properties by model checking, thus showing the applicability of our approach in practice. Categories and Subj...

• Type: Conference
• Year: 2008
• Where: CODES
• Authors: Paula Herber, Joachim Fellmuth, Sabine Glesner
• Keywords: CODES 2008, Software Engineering, SystemC, SystemC Designs, Uppaal Model