Improving System-Level Verification of SystemC Models with SPIN

Authors Martin Elshuber, Susanne Kandl, Peter Puschner

Thumbnail PDF


  • Filesize: 336 kB
  • 6 pages

Document Identifiers

Author Details

Martin Elshuber
Susanne Kandl
Peter Puschner

Cite AsGet BibTex

Martin Elshuber, Susanne Kandl, and Peter Puschner. Improving System-Level Verification of SystemC Models with SPIN. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 74-79, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)


SystemC is a de-facto industry standard for developing, modelling, and simulating embedded systems. As embedded systems become more and more integrated into many aspects of human lives (e.g., transportation, surveillance systems, ...), failures of embedded systems might cause dangerous hazards to individuals or groups. Guaranteeing safety of such systems makes formal verification crucial. In this paper we present a novel approach for verifying SystemC models with SPIN. Focusing on system-level verification we reuse compiled and executable code from the original model and embed it into the verifier generated by SPIN. In contrast to most other approaches, which require a complete model transformation, in our approach the transformation focuses only on the relevant parts of the model while leaving functional blocks untransformed. Our technique aims at reducing the state vector size managed by the verifier of SPIN, at improving state exploration performance by avoiding unnecessary model transformation steps, and at concentrating on verifying properties that emerge from the composition of multiple functional units.
  • SystemC
  • SPIN
  • Promela
  • System-Level Verification


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail