search query: @keyword Uppaal / total: 2
reference: 1 / 2
« previous | next »
Author: | Lahtinen, Jussi |
Title: | Model checking timed safety instrumented systems |
Ajastettujen turva-automaatiojärjestelmien mallintarkastuksesta | |
Publication type: | Master's thesis |
Publication year: | 2008 |
Pages: | vii + 57 Language: eng |
Department/School: | Informaatio- ja luonnontieteiden tiedekunta |
Main subject: | Tietojenkäsittelyteoria (T-119) |
Supervisor: | Niemelä, Ilkka |
Instructor: | Heljanko, Keijo |
OEVS: | Electronic archive copy is available via Aalto Thesis Database.
Instructions Reading digital theses in the closed network of the Aalto University Harald Herlin Learning CentreIn the closed network of Learning Centre you can read digital and digitized theses not available in the open network. The Learning Centre contact details and opening hours: https://learningcentre.aalto.fi/en/harald-herlin-learning-centre/ You can read theses on the Learning Centre customer computers, which are available on all floors.
Logging on to the customer computers
Opening a thesis
Reading the thesis
Printing the thesis
|
Location: | P1 Ark Aalto | Archive |
Keywords: | safety instrumented systems model checking real-time Uppaal turva-automaatiojärjestelmät mallintarkastus reaali-aika Uppaal |
Abstract (fin): | 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. |
ED: | 2008-08-22 |
INSSI record number: 36067
+ add basket
« previous | next »
INSSI