Counterexample analysis for automated refinement of data abstracted state machine models

Thumbnail Image

URL

Journal Title

Journal ISSN

Volume Title

Helsinki University of Technology | Master's thesis
Checking the digitized thesis and permission for publishing
Instructions for the author
Location:
P1 Ark Aalto

Authors

Date

2008

Department

Informaatio- ja luonnontieteiden tiedekunta

Major/Subject

Tietojenkäsittelyteoria

Mcode

T-119

Degree programme

Language

en

Pages

viii + 68

Series

Abstract

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.

Description

Supervisor

Niemelä, Ilkka

Thesis advisor

Tauriainen, Heikki

Keywords

model checking, mallintarkistus, data abstraction, abstrahoidut tietotyypit, refinement, abstraktion hienonnus, UML, UML, state machines, tilakoneet

Other note

Citation

Permanent link to this item

https://urn.fi/URN:NBN:fi:aalto-2020120554889

Collections

[dipl] Teknillinen korkeakoulu / TKK