Mallipohjainen testigenerointi vuoanalyysin ohjaamalla symbolisella suorittimella

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ä