2026-07-21T23:33:25Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3589 2024-03-06T10:29:02Z ddc:004 open_access

Verification of Safety-Critical Systems: A Case Study Report on Using Modern Model Checking Tools Jääskeläinen, Antti Katara, Mika Katz, Shmuel Virtanen, Heikki Functional safety SIL-3 model checking tools 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Antti Jääskeläinen and Mika Katara and Shmuel Katz and Heikki Virtanen 2012 Is Part Of OASIcs, Volume 24, 6th International Workshop on Systems Software Verification (2012) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.SSV.2011.44 urn:nbn:de:0030-drops-35891 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SSV.2011.44 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode