Applying model checking to analysing safety instrumented systems
No Thumbnail Available
URL
Journal Title
Journal ISSN
Volume Title
Helsinki University of Technology |
Diplomityö
Checking the digitized thesis and permission for publishing
Instructions for the author
Instructions for the author
Authors
Date
2008
Major/Subject
Tietojenkäsittelyteoria
Mcode
T-119
Degree programme
Tietotekniikan tutkinto-ohjelma
Language
en
Pages
viii + 68
Series
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.Description
Supervisor
Niemelä, IlkkaThesis advisor
Heljanko, KeijoKeywords
model checking, mallintarkastus, safety instrumented systems, turva-automaatiojärjestelmät