License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.FSFMA.2013.74
URN: urn:nbn:de:0030-drops-40915
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4091/
Go to the corresponding OASIcs Volume Portal

Elshuber, Martin ; Kandl, Susanne ; Puschner, Peter

Improving System-Level Verification of SystemC Models with SPIN

pdf-format:
11.pdf (0.3 MB)

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.

BibTeX - Entry

@InProceedings{elshuber_et_al:OASIcs:2013:4091,
  author =	{Martin Elshuber and Susanne Kandl and Peter Puschner},
  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 =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-56-9},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{31},
  editor =	{Christine Choppy and Jun Sun},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4091},
  URN =		{urn:nbn:de:0030-drops-40915},
  doi =		{10.4230/OASIcs.FSFMA.2013.74},
  annote =	{Keywords: SystemC, SPIN, Promela, System-Level Verification}
}

Keywords: SystemC, SPIN, Promela, System-Level Verification
Collection: 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)
Issue Date: 2013
Date of publication: 14.07.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI