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

Antti JääSkeläInen, Mika Katara, Shmuel Katz & Heikki Virtanen
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...