haku: @keyword reachability analysis / yhteensä: 13
viite: 10 / 13
Tekijä: | Heljanko, Keijo |
Työn nimi: | Model Checking the Branching Time Temporal Logic CTL |
Haarautuvan ajan temporaalilogiikan CTL mallintarkastus | |
Julkaisutyyppi: | Diplomityö |
Julkaisuvuosi: | 1997 |
Sivut: | vii + 71 s. + 3 Kieli: eng |
Koulu/Laitos/Osasto: | Tietotekniikan osasto |
Oppiaine: | Digitaalitekniikka (Tik-79) |
Valvoja: | Ojala, Leo |
Ohjaaja: | Lilius, Johan |
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 T80 | Arkisto |
Avainsanat: | model checking temporal logic verification reachability analysis state-space exploration PROD mallintarkastus temporaalilogiikka CTL verifiointi saavutettavuusanalyysi tila-avaruuden tutkinta PROD |
Tiivistelmä (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 tietueen numero: 12043
+ lisää koriin
INSSI