search query: @keyword symbolinen suoritus / total: 5
reference: 2 / 5
« previous | next »
Author:Lahola, Mikko
Title:Flow analysis directed symbolic execution for model-based test generation
Mallipohjainen testigenerointi vuoanalyysin ohjaamalla symbolisella suorittimella
Publication type:Master's thesis
Publication year:2010
Pages:x + 57      Language:   eng
Department/School:Informaatio- ja luonnontieteiden tiedekunta
Main subject:Tietojenkäsittelyteoria   (T-119)
Supervisor:Niemelä, Ilkka
Instructor:Huima, Antti
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 Centre

In 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

  • Aalto University staff members log on to the customer computer using the Aalto username and password.
  • Other customers log on using a shared username and password.

Opening a thesis

  • On the desktop of the customer computers, you will find an icon titled:

    Aalto Thesis Database

  • Click on the icon to search for and open the thesis you are looking for from Aaltodoc database. You can find the thesis file by clicking the link on the OEV or OEVS field.

Reading the thesis

  • You can either print the thesis or read it on the customer computer screen.
  • You cannot save the thesis file on a flash drive or email it.
  • You cannot copy text or images from the file.
  • You cannot edit the file.

Printing the thesis

  • You can print the thesis for your personal study or research use.
  • Aalto University students and staff members may print black-and-white prints on the PrintingPoint devices when using the computer with personal Aalto username and password. Color printing is possible using the printer u90203-psc3, which is located near the customer service. Color printing is subject to a charge to Aalto University students and staff members.
  • Other customers can use the printer u90203-psc3. All printing is subject to a charge to non-University members.
Location:P1 Ark Aalto     | Archive
Keywords:symbolic execution
flow analysis
model-based software testing
pushdown automata
symbolinen suoritus
vuoanalyysi
mallipohjainen ohjekmistotestaus
pinoautomaatit
Abstract (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.
Abstract (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ä.
ED:2010-08-27
INSSI record number: 40294
+ add basket
« previous | next »
INSSI