haku: @keyword mallintarkastus / yhteensä: 13
viite: 5 / 13
Tekijä: | Lahtinen, Jussi |
Työn nimi: | Model checking timed safety instrumented systems |
Ajastettujen turva-automaatiojärjestelmien mallintarkastuksesta | |
Julkaisutyyppi: | Diplomityö |
Julkaisuvuosi: | 2008 |
Sivut: | vii + 57 Kieli: eng |
Koulu/Laitos/Osasto: | Informaatio- ja luonnontieteiden tiedekunta |
Oppiaine: | Tietojenkäsittelyteoria (T-119) |
Valvoja: | Niemelä, Ilkka |
Ohjaaja: | Heljanko, Keijo |
OEVS: | Sähköinen arkistokappale on luettavissa Aalto Thesis Databasen kautta.
Ohje Digitaalisten opinnäytteiden lukeminen Aalto-yliopiston Harald Herlin -oppimiskeskuksen suljetussa verkossaOppimiskeskuksen suljetussa verkossa voi lukea sellaisia digitaalisia ja digitoituja opinnäytteitä, joille ei ole saatu julkaisulupaa avoimessa verkossa. Oppimiskeskuksen yhteystiedot ja aukioloajat: https://learningcentre.aalto.fi/fi/harald-herlin-oppimiskeskus/ Opinnäytteitä voi lukea Oppimiskeskuksen asiakaskoneilla, joita löytyy kaikista kerroksista.
Kirjautuminen asiakaskoneille
Opinnäytteen avaaminen
Opinnäytteen lukeminen
Opinnäytteen tulostus
|
Sijainti: | P1 Ark Aalto | Arkisto |
Avainsanat: | safety instrumented systems model checking real-time Uppaal turva-automaatiojärjestelmät mallintarkastus reaali-aika Uppaal |
Tiivistelmä (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 tietueen numero: 36067
+ lisää koriin
INSSI