Model Checking Large Nuclear Power Plant Safety System Designs

Abstract

Digital instrumentation and control (I & C) systems are increasingly being used for implementing safety-critical applications such as nuclear power plant safety systems. The exhaustive verification of these systems is challenging, and verification methods such as testing and simulation are typically insufficient. Model checking is a formal method for verifying the correctness of a system design model. The requirements of the system are formalised using temporal logic, and the behaviour of the system model is exhaustively analysed with respect to these formal specifications. The method is very effective in finding hidden design errors. Model checking is computationally very demanding, and thus one of the challenges in applying model checking is its scalability. This dissertation discusses the verification of larger systems implementing multiple functions using model checking. First of all, this dissertation presents methodology for modelling safety system designs, and describes a simple abstraction technique for models of these systems that utilises modular over-approximating abstractions. Furthermore, the dissertation presents the development of an iterative abstraction refinement algorithm for the purpose of automatically finding an abstraction level suitable for verification. This dissertation also studies hardware failures, and creates an extension of the safety system modelling methodology that enables the analysis of fault-tolerance properties in large many-redundant system assemblies. The methodology follows closely the conventions of probabilistic risk assessment (PRA), and serves as a first step for further integration between model checking and PRA. Finally, this work presents the development of a test set generation technique based on model checking that utilises the structure of function block diagram (FBD) programs. The results of this work have a high significance to safety because the developed techniques can be used to verify the correctness of safety system designs used in nuclear power plants. The work has also improved the scalability and applicability of model checking, and can be seen as part of a continuum toward larger plant-level models and toward new all-encompassing safety analysis approaches.

Monet turvakriittiset sovellukset kuten ydinvoimaloissa käytetyt turva-automaatiojärjestelmät perustuvat yhä enenevässä määrin digitaaliseen ohjelmoitavaan tekniikkaan. Tällaisten digitaalisten järjestelmien verifiointi on erittäin haastavaa, eivätkä perinteiset menetelmät kuten testaus ja simulointi usein kykene saavuttamaan täydellistä kattavuutta. Mallintarkastus on formaali menetelmä, jota käytetään järjestelmän verifioinnin apuvälineenä. Mallintarkastuksessa järjestelmän toiminnalliset vaatimukset muodostetaan aikalogiikan lauseiden avulla, ja vaatimusten täyttyminen tarkastetaan käymällä systemaattisesti läpi kaikki järjestelmästä laaditun mallin käyttäytymiset. Menetelmä on erittäin tehokas löytämään piileviä suunnitteluvirheitä. Mallintarkastus on laskennallisesti vaativa menetelmä, ja eräs menetelmän soveltamiseen liittyvä haaste on sen skaalautuvuus. Tässä väitöstyössä tutkitaan mallintarkastuksen soveltamista useiden alijärjestelmien muodostamien laajojen kokonaisuuksien verifiointiin. Työssä on luotu metodologiaa turvajärjestelmien mallintamiseen, sekä tehty mallinnustavan kanssa yhteensopiva modulaarinen abstraktiomenetelmä, joka perustuu moduulien yliapproksimatiivisiin abstraktioihin. Lisäksi väitöstyössä on kehitetty iteratiivinen tekniikka, jonka tarkoituksena on etsiä verifiointiin sopiva abstraktiotaso automaattisesti. Työssä on myös tutkittu laitteistovikojen mallintamista ja kehitetty turvajärjestelmien mallinnuksen kanssa yhteensopiva mallinnustekniikka, joka mahdollistaa järjestelmän vikasietoisuuteen liittyvien ominaisuuksien tarkastelemisen laajoissa moniredundanttisissa järjestelmissä. Tekniikka mukailee todennäköisyysperusteisen riskianalyysin (PRA, probabilistic risk assessment) käyttämiä tapoja jäsentää vikaantumiseen liittyviä ongelmia, ja on täten myös askel kohti näiden kahden menetelmän syvempää integraatiota. Viimeiseksi, työssä on kehitetty mallintarkastusta hyödyntävä tekniikka, jonka avulla voidaan automaattisesti luoda joukko testejä toimilohko-kaavion (function block diagram, FBD) rakenteen perusteella. Väitöstyön tulokset ovat tärkeitä turvallisuuden kannalta, sillä kehitettyjä tekniikoita voidaan käyttää varmistamaan turva-automaatiojärjestelmien suunnittelun virheettömyys. Väitöstyön myötä mallintarkastuksen skaalautuvuus ja käyttökelpoisuus ovat myös parantuneet. Työn voi nähdä osana jatkumoa kohti yhä suurempia laitostason malleja, ja uusia kokonaisvaltaisia tapoja analysoida turvallisuutta.