License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.SSV.2011.44
URN: urn:nbn:de:0030-drops-35891
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3589/
Go to the corresponding OASIcs Volume Portal

Jääskeläinen, Antti ; Katara, Mika ; Katz, Shmuel ; Virtanen, Heikki

Verification of Safety-Critical Systems: A Case Study Report on Using Modern Model Checking Tools

pdf-format:
5.pdf (0.4 MB)

Abstract

paper, we describe a case study where a simple 2oo3 voting scheme for a shutdown system was verified using two bounded model checking tools, CBMC and EBMC. The system represents Systematic Capability level 3 according to IEC 61508 ed2.0. The verification process was based on requirements and pseudo code, and involved verifying C and Verilog code implementing the pseudo code. The results suggest that the tools were suitable for the task, but require considerable
training to reach productive use for code embedded in industrial equipment. We also identified some issues in the development process that could be streamlined with the use of more formal verification methods. Towards the end of the paper, we discuss the issues we found and how to address them in a practical setting.

BibTeX - Entry

@InProceedings{jskelinen_et_al:OASIcs:2012:3589,
  author =	{Antti J{\"a}{\"a}skel{\"a}inen and Mika Katara and Shmuel Katz and Heikki Virtanen},
  title =	{{Verification of Safety-Critical Systems: A Case Study Report on Using Modern Model Checking Tools}},
  booktitle =	{6th International Workshop on Systems Software Verification},
  pages =	{44--56},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-36-1},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{24},
  editor =	{J{\"o}rg Brauer and Marco Roveri and Hendrik Tews},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3589},
  URN =		{urn:nbn:de:0030-drops-35891},
  doi =		{10.4230/OASIcs.SSV.2011.44},
  annote =	{Keywords: Functional safety, SIL-3, model checking, tools}
}

Keywords: Functional safety, SIL-3, model checking, tools
Collection: 6th International Workshop on Systems Software Verification
Issue Date: 2012
Date of publication: 13.07.2012

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