search query: @keyword mallintarkistus / total: 2
reference: 1 / 2
« previous | next »
Author: | Ojala, Vesa |
Title: | Counterexample analysis for automated refinement of data abstracted state machine models |
Vastaesimerkkianalyysi abstrahoituja tietotyyppejä käyttävien tilakonemallien automaattiseen hienonnukseen | |
Publication type: | Master's thesis |
Publication year: | 2008 |
Pages: | viii + 68 Language: eng |
Department/School: | Informaatio- ja luonnontieteiden tiedekunta |
Main subject: | Tietojenkäsittelyteoria (T-119) |
Supervisor: | Niemelä, Ilkka |
Instructor: | Tauriainen, Heikki |
OEVS: | Electronic archive copy is available via Aalto Thesis Database.
Instructions Reading digital theses in the closed network of the Aalto University Harald Herlin Learning CentreIn the closed network of Learning Centre you can read digital and digitized theses not available in the open network. The Learning Centre contact details and opening hours: https://learningcentre.aalto.fi/en/harald-herlin-learning-centre/ You can read theses on the Learning Centre customer computers, which are available on all floors.
Logging on to the customer computers
Opening a thesis
Reading the thesis
Printing the thesis
|
Location: | P1 Ark Aalto | Archive |
Keywords: | model checking data abstraction refinement UML state machines mallintarkistus abstrahoidut tietotyypit abstraktion hienonnus UML tilakoneet |
Abstract (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 record number: 36663
+ add basket
« previous | next »
INSSI