Model Checking the Branching Time Temporal Logic CTL
No Thumbnail Available
Journal Title
Journal ISSN
Volume Title
Helsinki University of Technology |
Diplomityö
Checking the digitized thesis and permission for publishing
Instructions for the author
Instructions for the author
Author
Date
1997
Department
Major/Subject
Digitaalitekniikka
Mcode
Tik-79
Degree programme
Language
en
Pages
vii + 71 s. + 3
Series
Abstract
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.Description
Supervisor
Ojala, LeoThesis advisor
Lilius, JohanKeywords
model checking, mallintarkastus, temporal logic, temporaalilogiikka, verification, CTL, reachability analysis, verifiointi, state-space exploration, saavutettavuusanalyysi, PROD, tila-avaruuden tutkinta, PROD
