haku: @instructor Tauriainen, Heikki / yhteensä: 1
viite: 1 / 1
« edellinen | seuraava »
Tekijä: | Ojala, Vesa |
Työn nimi: | Counterexample analysis for automated refinement of data abstracted state machine models |
Vastaesimerkkianalyysi abstrahoituja tietotyyppejä käyttävien tilakonemallien automaattiseen hienonnukseen | |
Julkaisutyyppi: | Diplomityö |
Julkaisuvuosi: | 2008 |
Sivut: | viii + 68 Kieli: eng |
Koulu/Laitos/Osasto: | Informaatio- ja luonnontieteiden tiedekunta |
Oppiaine: | Tietojenkäsittelyteoria (T-119) |
Valvoja: | Niemelä, Ilkka |
Ohjaaja: | Tauriainen, Heikki |
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: | model checking data abstraction refinement UML state machines mallintarkistus abstrahoidut tietotyypit abstraktion hienonnus UML tilakoneet |
Tiivistelmä (fin): | Tarkastettavan järjestelmän tila-avaruuden valtava koko on ollut yksi suurimmista ongelmista mallintarkastuksessa, pienimpiä järjestelmiä lukuun ottamatta. Ongelman ratkaisemiseksi on kehitetty erilaisia abstraktiotekniikoita. Tässä työssä käytetään abstrahoituja tietotyyppejä tarkastettaessa assert-lauseiden pitävyyttä ja implisiittisten viestinkulutusten olemassaoloa asynkronisesti viestivistä tilakonemalleista. Abstrahoitua mallia tarkastettaessa saadut vastaesimerkit eivät välttämättä vastaa ainuttakaan suoritusta alkuperäisessä mallissa. Tällaiset valheelliset vastaesimerkit täytyy tunnistaa ja abstraktiota on hienonnettava valheellisen vastaesimerkin mahdollisuuden poistamiseksi abstrahoidusta-mallista. Tässä diplomityössä kuvataan, miten valheelliset vastaesimerkit voidaan tunnistaa. Työssä esitellään myös menetelmä oleellisten muuttujien ja olioiden löytämiseen suorituksen kussakin pisteessä tietovuoanalyysiä käyttäen. Nämä oleelliset paikat auttavat keskittymään muuttujiin, joiden tietotyyppejä hienontamalla saadaan valheellisen vastaesimerkin mahdollisuus abstraktiosta poistettua. Työssä esitellään myös menetelmä kokonaislukuvälejä abstrakteina tietotyyppeinään käyttävien mallien automaattiseen hienonnukseen. Menetelmä etsii sopivaa hienonnusta käyttämällä hyväkseen oleellisia paikkoja. Työssä esitellyt menetelmät on toteutettu osana SMUML-projektia (Symbolic Methods for UML Behavioural Diagrams) osaksi SMUML toolkit -ohjelmistoa. |
ED: | 2009-01-20 |
INSSI tietueen numero: 36663
+ lisää koriin
« edellinen | seuraava »
INSSI