Sciweavers

Share
CODES
2008
IEEE

Model checking SystemC designs using timed automata

9 years 1 months ago
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...
Paula Herber, Joachim Fellmuth, Sabine Glesner
Added 18 Oct 2010
Updated 18 Oct 2010
Type Conference
Year 2008
Where CODES
Authors Paula Herber, Joachim Fellmuth, Sabine Glesner
Comments (0)
books