Potential applications of model checking in probabilistic risk assessments

In model checking, a model of instrumentation and control (I&C) system’s application logic is created to formally verify the correct functioning of a system model by examining all of its possible behaviours. Model checking can provide important information on the failures of digital I&C systems and their software in particular.The integration of model checking with probabilistic risk assessment (PRA) modelling has been studied previously in two separate case studies. In the report, an overview to the common taxonomy of failure modes and current practices of modelling digital I&C systems in PRA is given. Findings from the previous case studies are reflected to the PRA modelling practices. Design issues identified by model checking in various VTT customer projects are compared to the failure modes and failure effects of software modules collected from different taxonomies for PRA.The case studies propose a coupling approach where the results of PRA are used to support model checking. The model checking analysis is restricted to a limited set of postulated hardware failures based on PRA results, potentially improving scalability of model checking. In this report, the focus is reversed and the focus is on studying how model checking can support PRA and its taxonomy.In order to use the model checking method as a support analysis for PRA modelling the complementary uses of the modelling methods should be developed. Potential complementary uses are for example: 1) The identification and analysis of extraordinary failure modes, including software failure modes, and potential detection of these failure modes; 2) Software reliability assessment of important functions; 3) The analysis and modelling of dynamic, i.e. time-dependent, features