1 Search Results for "Kandl, Susanne"


Document
Improving System-Level Verification of SystemC Models with SPIN

Authors: Martin Elshuber, Susanne Kandl, and Peter Puschner

Published in: OASIcs, Volume 31, 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)


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.

Cite as

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)


Copy BibTex To Clipboard

@InProceedings{elshuber_et_al:OASIcs.FSFMA.2013.74,
  author =	{Elshuber, Martin and Kandl, Susanne and Puschner, Peter},
  title =	{{Improving System-Level Verification of SystemC Models with SPIN}},
  booktitle =	{1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)},
  pages =	{74--79},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-56-9},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{31},
  editor =	{Choppy, Christine and Sun, Jun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.74},
  URN =		{urn:nbn:de:0030-drops-40915},
  doi =		{10.4230/OASIcs.FSFMA.2013.74},
  annote =	{Keywords: SystemC, SPIN, Promela, System-Level Verification}
}
  • Refine by Author
  • 1 Elshuber, Martin
  • 1 Kandl, Susanne
  • 1 Puschner, Peter

  • Refine by Classification

  • Refine by Keyword
  • 1 Promela
  • 1 SPIN
  • 1 System-Level Verification
  • 1 SystemC

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2013

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail