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

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



PDF
Thumbnail PDF

File

OASIcs.SSV.2011.44.pdf
  • Filesize: 362 kB
  • 13 pages

Document Identifiers

Author Details

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

Cite AsGet BibTex

Antti Jääskeläinen, Mika Katara, Shmuel Katz, and Heikki Virtanen. Verification of Safety-Critical Systems: A Case Study Report on Using Modern Model Checking Tools. In 6th International Workshop on Systems Software Verification. Open Access Series in Informatics (OASIcs), Volume 24, pp. 44-56, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
https://doi.org/10.4230/OASIcs.SSV.2011.44

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.
Keywords
  • Functional safety
  • SIL-3
  • model checking
  • tools

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
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