Applying model checking to analysing safety instrumented systems

Abstract

Teollisuudessa on käynnissä muutosprosessi, jossa vanhoja analogisia instrumentointi- ja säätöjärjestelmiä korvataan uusilla digitaalisilla vastineilla. Uudet digitaaliset järjestelmät mahdollistavat yhä monipuolisempia säätötehtäviä ja etenkin niiden käyttö turva-automaatiossa on synnyttänyt tarpeen uusille verifiointimenetelmille. Tämä työ pyrkii vastaamaan tähän tarpeeseen.

Työn tavoitteena on tutkia mallintarkastusmenetelmän soveltuvuutta todelliseen teollisuudessa käytettävään turva-automaatiojärjestelmään ja tutkia, voidaanko tällainen järjestelmä mallintaa tasolla, joka mahdollistaa relevanttien turvaominaisuuksien verifioinnin ja joka toisaalta säilyttää mallin analysoitavan kokoisena. Keskeisenä tavoitteena on myös luoda yleinen metodologia mallintarkastusmenetelmän soveltamiseksi turva-automaatiojärjestelmiin.

Tapaustutkimuksena kuvattiin UTU Falcon -merkkiseen valokaarisuojaukseen perustuva suojajärjestelmä käyttöympäristöineen NuSMV kuvauskielellä ja tarkastettiin kyseinen malli oleellisimpien turvaominaisuuksien suhteen.

Tutkimustulokset osoittavat, että mallintarkastus vaikuttaa lupaavalta menetelmältä turva-automaatiojärjestelmien verifiointiin.