arvutiteaduse instituudi lõputööderegister


Deklaratiivsete protsessimudelite avastamine sündmuste logist kasutades temporaalloogika päringuid
Nimi Margus Räim
Kokkuvõte Käesolev magistritöö keskendub protsessile seatud piirangute avastamisele sündmuste logist, mida saab väljendada temporaalloogika abil. Piirangute avastamise meetodina kasutame temporaalloogika päringute kontrollimist sündmuste logi vastu. Temporaalloogika päring on modaalloogika avaldis, mis sisaldab muutujaid, mis võtavad oma väärtuse automaarpropositsioonide hulgast. Temporaalloogika päring käivitatakse vastu olekumasinat, mis on konstrueeritud sündmuste logi järgi. Päringu tulemuseks on kõik temporaalloogika avaldised, kus muutujad on asendatud kõikvõimalike automaarpropositsioonidega, mis muudavad avaldise tõeseks antud olekumasinas. See meetod ei vaja protsessi piirangute avastamiseks negatiivseid näiteid (protsessi juhtumid, mis ei tohi aset leida) sündmuste logis nagu osa avaldatuid meetodeid vajab. See meetod samuti laiendab võimalike avastatavate piirangute hulka võrreldes olemas olevate meetoditega.
Lõputöö keel inglise
Lõputöö tüüp Magister - Tarkvaratehnika
Juhendaja(d) Fabrizio M. Maggi
Kaitsmise aasta 2014
PDF