haku: @keyword symbolic execution / yhteensä: 2
hakutulos-lista
viite: 1 / 2
« edellinen | seuraava »
Tekijä:Lahola, Mikko
Työn nimi:Flow analysis directed symbolic execution for model-based test generation
Mallipohjainen testigenerointi vuoanalyysin ohjaamalla symbolisella suorittimella
Julkaisutyyppi:Diplomityö
Julkaisuvuosi:2010
Sivut:x + 57      Kieli:   eng
Koulu/Laitos/Osasto:Informaatio- ja luonnontieteiden tiedekunta
Oppiaine:Tietojenkäsittelyteoria   (T-119)
Valvoja:Niemelä, Ilkka
Ohjaaja:Huima, Antti
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:symbolic execution
flow analysis
model-based software testing
pushdown automata
symbolinen suoritus
vuoanalyysi
mallipohjainen ohjekmistotestaus
pinoautomaatit
Tiivistelmä (fin): Ohjelmistotestauksessa käytettyjä testitapauksia on tuotettu käyttäen formaaleja ohjelma-analyysimenetelmiä.
Menetelmien etuna on, että testit voidaan tuottaa vähemmällä työmäärällä saaden niistä kuitenkin käsintehtyjä parempilaatuisia.
Menetelmien yleisenä tehokkuusongelmana on kuitenkin analysoitavien ohjelmien tila-avaruuden valtava koko.

Työssä tarkastellaan mallipohjaisessa testauksessa käytetyn testitapauksia tuottavan teollisen ohjelmiston tehostamista.
Ohjelmisto käyttää symbolinen suoritus -tyyppistä ohjelma-analyysimenetelmää etsiäkseen suorituspolun mallin jokaiseen syntaktiseen kontrollivuon pisteeseen.
Teollisuuskäytöstä johtuen ohjelmiston on käsiteltävä äärettömän tila-avaruuden malleja ja siksi ohjelmiston symbolisessa suorittimessa on asetettu raja käsiteltävien suorituspolkujen pituudelle.

Työssä esitetään symbolisen suorituksen tekemää suorituspolkujen etsintää optimoiva tekniikka.
Idealla on, että vain ne suorituspolut, jotka saavuttavat uusia syntaktisia kontrollivuon pisteitä annetun rajan puitteissa, ovat oleellisia.
Oleellisten polkujen tunnistamiseksi lasketaan rakenne, joka esittää turvallista yliapproksimaatiota mallin mahdollisille suorituspoluille ja verrataan suoritusaikaisesti rakenteesta löytyvien suorituspolkujen pituuksia annettuun haun rajaan.
Rakenne tuotetaan kääntäjätekniikassa yleisesti käytetyllä vuoanalyysimenetelmällä.

Työssä esitetään myös algoritmi vuoanalyysin tuottaman pinoautomaattirakenteen minimipolkulaskennalle.
Esitellyn optimointitekniikan vaikutusta ohjelmiston symbolisen suorittimen tehokkuuteen ja minimipolkulaskennan tehokkuutta arvioidaan kokeellisesti teollisuusesimerkeillä.
Tiivistelmä (eng): Formal program analysis methods have been used to aid test case generation for software testing for some time now due to their ability to generate tests with less labour and of better quality than those done by manual means.
However, the performance of the methods is commonly hampered by state space explosion.

In the thesis the focus is on improving the performance of an industrial-strength tool that generates tests in a model-based testing setting.
The tests are generated with a program analysis method called symbolic execution that finds execution paths to syntactic control flow points of the model.
The industrial setting requires that the tool can handle infinite-state models, and to this effect, the execution path lengths are bounded in the symbolic execution system.

The thesis presents a technique to optimize the execution path search performed by the symbolic execution system.
The optimization is based on the idea that only the execution paths that reach new syntactic control flow points within the given bound are relevant to the search.
To identify the relevant paths, a structure containing a safe over approximation of the possible execution paths of the model is computed, and during symbolic execution path lengths in the structure are compared to the search bound.
The structure is computed with a common compiler technique called flow analysis.

Also, as the structure is chosen to be equivalent to a pushdown automaton the thesis presents an algorithm to calculate shortest paths in pushdown automata.
The impact of the search optimization technique and the efficiency of the shortest path calculation algorithm are empirically quantified with industrial models.
ED:2010-08-27
INSSI tietueen numero: 40294
+ lisää koriin
« edellinen | seuraava »
INSSI