search query: @keyword saavutettavuusanalyysi / total: 13
reference: 11 / 13
Author: | Heljanko, Keijo |
Title: | Model Checking the Branching Time Temporal Logic CTL |
Haarautuvan ajan temporaalilogiikan CTL mallintarkastus | |
Publication type: | Master's thesis |
Publication year: | 1997 |
Pages: | vii + 71 s. + 3 Language: eng |
Department/School: | Tietotekniikan osasto |
Main subject: | Digitaalitekniikka (Tik-79) |
Supervisor: | Ojala, Leo |
Instructor: | Lilius, Johan |
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 T80 | Archive |
Keywords: | model checking temporal logic verification reachability analysis state-space exploration PROD mallintarkastus temporaalilogiikka CTL verifiointi saavutettavuusanalyysi tila-avaruuden tutkinta PROD |
Abstract (fin): | Saavutettavuus-analyysi on menetelmä jolla voidaan analysoida rinnakkaisen järjestelmän dynaamista käyttäytymistä. Yksi tapa määritellä järjestelmän käyttäytymiseltä vaadittavia ominaisuuksia on käyttää haarautuvan ajan temporaalilogiikkaa CTL. Mallintarkastuksella tutkitaan, täyttääkö järjestelmän käyttäytyminen siltä vaaditun ominaisuuden. Työssä analysoidaan useita mallintarkastus algoritmejä CTL:lle. Työn päätulos on uusi mallintarkastus algoritmi, joka aikakompleksisuudeltaan vastaa parhaita aikaisemmin esitettyjä algoritmejä, ja muistivaatimuksiltaan on joko yhtä hyvä tai vähemmän muistia vaativa kuin aikaisemmin esitetyt algoritmit, riippuen tutkittavan järjestelmän rakenteesta. Algoritmi sisältää lisäksi vastaesimerkki- ja todistaja-polun etsintä ominaisuuden, joka on hyödyllinen kun järjestelmän virheellisen käytöksen syytä pyritään etsimään. Esitetty algoritmi on myös hyvin suoraviivainen toteuttaa tehokkaalla tavalla, ja työssä algoritmi on toteutettu PROD työkalu-ohjelmistoon. |
ED: | 1997-04-08 |
INSSI record number: 12043
+ add basket
INSSI