Title: | Model Checking Large Nuclear Power Plant Safety System Designs Ydinvoimaloiden laajojen turva-automaatiojärjestelmien mallintarkastus |
Author(s): | Lahtinen, Jussi |
Date: | 2016 |
Language: | en |
Pages: | 165 + app. 75 |
Department: | Tietotekniikan laitos Department of Computer Science |
ISBN: | 978-952-60-6958-6 (Aalto, electronic) 978-952-60-6959-3 (Aalto, printed) 978-951-38-8447-5 (VTT, electronic) 978-951-38-8448-2 (VTT, printed) |
Series: | Aalto University publication series DOCTORAL DISSERTATIONS, 159/2016, VTT Science, 133 |
ISSN: | 1799-4942 (Aalto, electronic) 1799-4934 (Aalto, printed) 1799-4934 (Aalto, ISSN-L) 2242-1203 (VTT, electronic) 2242-119X (VTT, printed) 2242-119X (VTT, ISSN-L) |
Supervising professor(s): | Heljanko, Keijo, Assoc. Prof., Aalto University, Department of Computer Science, Finland |
Thesis advisor(s): | Heljanko, Keijo, Assoc. Prof., Aalto University, Department of Computer Science, Finland |
Subject: | Computer science |
Keywords: | model checking, automation, nuclear power plants, PLC, Function Block Diagram, fault-tolerance, instrumentation and control I & C, iterative abstraction refinement, compositional minimization, formal verification, safety system, structure-based testing, test generation, mallintarkastus, automaatio, ydinvoima, toimilohko, vikasietoisuus, abstraktio, formaali verifiointi, turvajärjestelmä, rakenteellinen testaus, testigenerointi |
Archive | yes |
|
|
Abstract: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. |
|
Parts:[Publication 1]: Jussi Lahtinen, Janne Valkonen, Kim Bjorkman, Juho Frits, Ilkka Niemela and Keijo Heljanko. Model checking of safety critical software in the nuclear engineering domain. Reliability Engineering & System Safety, Vol. 105, p.104 – 113, Elsevier, September 2012. DOI: 10.1016/j.ress.2012.03.021 View at Publisher [Publication 2]: Jussi Lahtinen, Kim Bjorkman, Janne Valkonen, Ilkka Niemela. Emergency diesel generator control system verification by model checking and compositional minimization. In 8th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2012), Znojmo, Czech Republic. Antonin Kucera, Thomas A. Henzinger, Jaroslav Nesetril, Tomas Vojnar and David Antos (Eds), p. 49 – 60, NOVPRESS, October 2012, ISBN 978-80-87342-15-2.[Publication 3]: Jussi Lahtinen, Tuomas Kuismin and Keijo Heljanko. Verifying large modular systems using iterative abstraction refinement. Reliability Engineering & System Safety, Vol. 139, p. 120 – 130, Elsevier, July 2015. DOI: 10.1016/j.ress.2015.03.012 View at Publisher [Publication 4]: Jussi Lahtinen. Verification of fault-tolerant system architectures using model checking. In 1st International Workshop on Development, Verification and Validation of Critical Systems (DEVVARTS), Lecture Notes in Computer Science, Vol. 8696, p. 195 – 206, Springer, September 2014. DOI: 10.1007/978-3-319-10557-4_23 View at Publisher [Publication 5]: Jussi Lahtinen. Automatic test set generation for function block based systems using model checking. In 9th International Conference on the Quality of Information and Communications Technology (QUATIC 2014), Guimaraes, Portugal, p. 216 – 225, IEEE, September 2014. DOI: 10.1109/QUATIC.2014.15 View at Publisher |
|
|
Unless otherwise stated, all rights belong to the author. You may download, display and print this publication for Your own personal use. Commercial use is prohibited.
Page content by: Aalto University Learning Centre | Privacy policy of the service | About this site