OASIcs.SSV.2011.44.pdf
- Filesize: 362 kB
- 13 pages
Document
Verification of Safety-Critical Systems: A Case Study Report on Using Modern Model Checking Tools
Authors
-
Part of:
Volume:
6th International Workshop on Systems Software Verification (SSV 2011)
Series: Open Access Series in Informatics (OASIcs) - License:
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
- Publication Date: 2012-07-13
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
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)
0PDF Downloads