Model checking reveals hidden errors in safety-critical I&C software

Model checking is an efficient formal method for the verification of (hardware or software) system designs. Through exhaustive analysis, hidden errors can be found in systems that have already undergone conventional V&V. In addition to several research projects, VTT has been consulting the Finnish Radiation and Nuclear Safety Authority (STUK) on evaluating nuclear power plant I&C system designs using model checking since 2008. In this paper, we present methods for easing the process of model checking of function block based I&C softwar