Oops! Examples of I&C design issues detected with model checking

Since 2008, VTT has used a formal verification method called model checking to verify instrumentation and control (I&C) application logic design in practical projects in the Finnish nuclear industry. In this paper, we present seven examples of the 66 confirmed design issues that we have detected. We then discuss potential causes why only formal verification revealed the otherwise hidden issues. We hope the examples will be useful in case studies related to verification and quality assurance of I&C