1. 1

Abstract highlights: “Despite the benefits, model checking is still not widely adopted in the verification of I&C systems, one exception being the Finnish nuclear industry. Since 2008, VTT has applied model checking in practical customer work related to… nuclear power plants. In this paper, we look at how the method has been used in each of these three projects. We also introduce a user-friendly, graphical modelling tool called MODCHK. We then present an overall view of the design issues detected during nine years of customer work, and one practical example. The 100% coverage means that the design errors that are found often relate to scenarios that are otherwise hard to account for (e.g., exact timing of events, or improper operator actions).”