haku: @keyword model checking / yhteensä: 20
hakutulos-lista
viite: 8 / 20
« 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
sulje

Digitaalisten opinnäytteiden lukeminen Aalto-yliopiston Harald Herlin -oppimiskeskuksen suljetussa verkossa

Oppimiskeskuksen 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

  • Aalto-yliopistolaiset kirjautuvat asiakaskoneille Aalto-tunnuksella ja salasanalla.
  • Muut asiakkaat kirjautuvat asiakaskoneille yhteistunnuksilla.

Opinnäytteen avaaminen

  • Asiakaskoneiden työpöydältä löytyy kuvake:

    Aalto Thesis Database

  • Kuvaketta klikkaamalla pääset hakemaan ja avaamaan etsimäsi opinnäytteen Aaltodoc-tietokannasta. Opinnäytetiedosto löytyy klikkaamalla viitetietojen OEV- tai OEVS-kentän linkkiä.

Opinnäytteen lukeminen

  • Opinnäytettä voi lukea asiakaskoneen ruudulta tai sen voi tulostaa paperille.
  • Opinnäytetiedostoa ei voi tallentaa muistitikulle tai lähettää sähköpostilla.
  • Opinnäytetiedoston sisältöä ei voi kopioida.
  • Opinnäytetiedostoa ei voi muokata.

Opinnäytteen tulostus

  • Opinnäytteen voi tulostaa itselleen henkilökohtaiseen opiskelu- ja tutkimuskäyttöön.
  • Aalto-yliopiston opiskelijat ja henkilökunta voivat tulostaa mustavalkotulosteita Oppimiskeskuksen SecurePrint-laitteille, kun tietokoneelle kirjaudutaan omilla Aalto-tunnuksilla. Väritulostus on mahdollista asiakaspalvelupisteen tulostimelle u90203-psc3. Väritulostaminen on maksullista Aalto-yliopiston opiskelijoille ja henkilökunnalle.
  • Ulkopuoliset asiakkaat voivat tulostaa mustavalko- ja väritulosteita Oppimiskeskuksen asiakaspalvelupisteen tulostimelle u90203-psc3. Tulostaminen on maksullista.
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