Flow analysis directed symbolic execution for model-based test generation
No Thumbnail Available
URL
Journal Title
Journal ISSN
Volume Title
School of Science |
Master's thesis
Checking the digitized thesis and permission for publishing
Instructions for the author
Instructions for the author
Authors
Date
2010
Major/Subject
Tietojenkäsittelyteoria
Mcode
T-119
Degree programme
Language
en
Pages
x + 57
Series
Abstract
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.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ä.Description
Supervisor
Niemelä, IlkkaThesis advisor
Huima, AnttiKeywords
symbolic execution, symbolinen suoritus, flow analysis, vuoanalyysi, model-based software testing, mallipohjainen ohjekmistotestaus, pushdown automata, pinoautomaatit