direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Page Content

Publications

Model Checking SystemC Designs Using Timed Automata
Citation key Herber08
Author Paula Herber and Joachim Fellmuth and Sabine Glesner
Title of Book Proceedings of the 6th International Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS)
Year 2008
Journal 6th International Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS 2008)
Organization ACM
Abstract 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.
Bibtex Type of Publication Conference Article
Link to original publication Download Bibtex entry

Zusatzinformationen / Extras

Quick Access:

Schnellnavigation zur Seite über Nummerneingabe