[Back]


Talks and Poster Presentations (with Proceedings-Entry):

M. Elshuber, S. Kandl, P. Puschner:
"Improving System-Level Verification of SystemC Models with SPIN";
Talk: 1st French Singaporean Workshop on Formal Methods and Applications, Singapore; 2013-07-15 - 2013-07-16; in: "1st French Singaporean Workshop on Formal Methods and Applications", (2013), ISBN: 978-3-939897-56-9; 6 pages.



English abstract:
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.

Keywords:
SystemC, SPIN, Promela, System-Level Verification


"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.4230/OASIcs.FSFMA.2013.74