Model checking timed safety instrumented systems

Thumbnail Image

URL

Journal Title

Journal ISSN

Volume Title

Helsinki University of Technology | Diplomityö
Checking the digitized thesis and permission for publishing
Instructions for the author

Authors

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