News

Model checking verifies the correctness of nuclear power plant safety systems

The study utilises model checking to address the insufficiencies of testing and simulation in the verification of safety systems.

Model checking as a process.

The object of Jussi Lahtinen’s dissertation was to find a more formal and mathematical approach to system verification and to develop model checking practices that are suitable for the nuclear industry. The traditional system verification methods, such as testing and simulation, do not have enough coverage to address the increasing digitalisation of safety automation systems.

         ‘Nuclear power plants have large safety systems in place that encompass multiple safety functions, such as the emergency diesel generator control system. In one of the techniques now developed, the system is divided into modules, and an algorithm is used for pinpointing the subset of modules that verifies the correctness of the system,’ says Lahtinen, explaining the practical implementation of the study.

At the architecture level, hardware failures in the microcircuits used for computing a number of functions, for example, are of pronounced significance. An individual software failure, on the other hand, is not all that safety-critical, given that the plant has a number of independent software-based safety systems in place.

         ‘Model checking is a highly effective method for finding latent design errors that may also be strange or unusual. Unlike testing or simulation, model checking is capable of achieving complete sequential coverage with respect to the requirement being examined,’ Lahtinen adds.

In the concluding phase of the dissertation, a method to support the structure-based testing of the function block diagrams used in the design of software-based systems was created. The method generates tests based on the structure of the function block diagram that describes the functioning of the safety automation system.

         ‘According to the feedback received from Fortum, the process of model checking as such may reveal errors that are easily ignored in testing. The comprehensive checking is also capable of analysing events over a very short time span,’ Lahtinen adds.

The results of the dissertation work have already been used in practical assignments for the Radiation and Nuclear Safety Authority concerning the Olkiluoto 3 project, for Fortum concerning the automation renewal of the Loviisa nuclear power plant, and for Fennovoima concerning the functional architecture of the foreseen Hanhikivi nuclear power plant. Further study on the integration of model checking with probabilistic risk analysis is already underway.

The dissertation work related to the study was supervised at the Aalto University Department of Computer Science by Professor Keijo Heljanko, and it was carried out at the VTT Technical Research Centre of Finland. A substantial part of the study was funded by the Finnish nuclear power plant safety research programme SAFIR. Model checking has been studied on a constant basis since 2007, and it is a very demanding method computationally.

More information:

Jussi Lahtinen
VTT
[email protected]
+3580 400 519 798

Keijo Heljanko
Professor
Department of Computer Science
[email protected]
+358 50 430 0771

Doctoral dissertation:  Model Checking Large Nuclear Power Plant Safety System Design

Defence of dissertation

  • Published:
  • Updated:
Share
URL copied!

Read more news

 Tutkimustyössä hyödynnetään Aalto-yliopiston radiokaiutonta huonetta Otaniemessä. Kuva: Aalto-yliopisto / Unto Rautio
Cooperation, Research & Art Published:

New doctoral programme focuses on the energy efficiency of radio waves

Nokia's donation to Aalto University will support research into new mobile communications systems, and particularly hardware development.
Kristo Ovaska, Kauppakorkeakoulun Vuoden Alumni 2022
Appointments Published:

Kristo Ovaska is the Alumnus of the Year 2022 of the School of Business

‘There is a great deal of demand for wide-ranging competence in the labour market,’ says Kristo Ovaska
Kuvassa näkyy vihreä kaurapelto ja digitaalisuutta kuvaavia 0- ja 1-merkkejä.
Research & Art Published:

Could carbon farming be scaled into a genuine alternative to industrialized agriculture?

In a new research project, researchers at the School of Business examine farmers' experiences of carbon farming to build understanding of the functioning of a new agricultural market.
A man wearing virtual reality glasses playing in a highly visualised extended reality world
Cooperation, Research & Art, University Published:

EMIL project: Open call and support for developing virtual worlds

The European Media and Immersion Lab (EMIL) project is launching its first open call for European extended reality developers.