aalto1 untyped-item.component.html
Model checking timed safety instrumented systems
Loading...
URL
Journal Title
Journal ISSN
Volume Title
Helsinki University of Technology |
Master's thesis
Electronic archive copy is available via Aalto Thesis Database.
Checking the digitized thesis and permission for publishing
Instructions for the author
Instructions for the author
Location:
Authors
Date
Major/Subject
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.