Model checking timed safety instrumented systems

No Thumbnail Available
Journal Title
Journal ISSN
Volume Title
Helsinki University of Technology | Diplomityö
Checking the digitized thesis and permission for publishing
Instructions for the author
Author
Date
2008
Department
Informaatio- ja luonnontieteiden tiedekunta
Major/Subject
Tietojenkäsittelyteoria
Mcode
T-119
Degree programme
Language
en
Pages
vii + 57
Series
Abstract
Turvallisuuskriittisissä ohjelmistojärjestelmissä olevat viat voivat aiheuttaa suuria taloudellisia sekä muita vahinkoja. Usein tällaiset järjestelmät ovat liian monimutkaisia, jotta ne voitaisiin testata kattavasti. Tämä työ käsittelee formaalia verifiointitekniikkaa nimeltään mallintarkastus. Tässä tekniikassa luodaan matemaattinen malli, joka toimii olennaisilta osiltaan samalla tavalla kuin tarkasteltava järjestelmä. Järjestelmän määrittelyt kuvataan jollain formaalilla kielellä, tyypillisesti aikalogiikalla. Mallin käyttäytyminen annetun määrittelyn suhteen voidaan tarkistaa tyhjentävästi. Tämä diplomityö käsittelee UTU Oy:n suunnittelemaa Falcon-nimistä valokaarisuojausjärjestelmää, jonka käyttäytymistä ohjaa ohjelmoitava logiikkaohjain (PLC). Järjestelmästä tehtiin kaksi erityyppistä mallia. Molemmat mallit koostuivat joukosta ajastettuja automaatteja. Ensimmäisessä mallissa ohjain toimi diskreeteillä aika-askelilla ja tietyllä taajuudella. Toisessa mallissa ohjain toimi ajon aikana muuttuvalla taajuudella jatkuvassa ajassa. Viisi järjestelmän määrittelyä laadittiin TCTL aikalogiikalla. Nämä määrittelyt verifioitiin molemmilla järjestelmän malleilla käyttämällä Uppaal-nimistä mallintarkastustyökalua. Verifioinnin laskenta-ajat mitattiin ja esitettiin. Diskreetin ajan mallin täytyi olla hyvin abstrakti, jotta se voitiin verifioida kohtuullisessa ajassa. Jatkuvan ajan malli kattoi enemmän käyttäytymistä kuin mallinnettava järjestelmä, ja se voitiin silti verifioida kohtuullisessa ajassa. Tässä mielessä jatkuvan ajan malli oli parempi kuin diskreettiaikainen malli. Tämän diplomityön kontribuutioita ovat ohjelmoitavan logiikkaohjaimen ohjaaman turva-automaatiojärjestelmän mallintarkastaminen, sekä erilaisten TCTL-määrittelyiden kuvaaminen Uppaal-työkalulle sopivassa muodossa. Työn tulokset osoittavat, että ajastettujen järjestelmien mallintarkastusta voidaan käyttää avuksi turva automaatiojärjestelmien verifioinnissa.
Description
Supervisor
Niemelä, Ilkka
Thesis advisor
Heljanko, Keijo
Keywords
safety instrumented systems, turva-automaatiojärjestelmät, model checking, mallintarkastus, real-time, reaali-aika, Uppaal, Uppaal
Other note
Citation
Permanent link to this item
https://urn.fi/URN:NBN:fi:aalto-2020120554559
Collections
[dipl] Teknillinen korkeakoulu / TKK