MC/DC Based Test Selection for Dynamic Symbolic Execution

 |  Login

Show simple item record

dc.contributor Aalto-yliopisto fi
dc.contributor Aalto University en
dc.contributor.author Kauttio, Janne
dc.date.accessioned 2013-10-29T12:16:19Z
dc.date.available 2013-10-29T12:16:19Z
dc.date.issued 2013
dc.identifier.uri https://aaltodoc.aalto.fi/handle/123456789/11203
dc.description.abstract Ensuring the correct operation of a software system is a relevant part of any software development process, but especially important for safety critical software systems used in aircrafts where failures can have fatal consequences and extreme reliability is required. As there is no official record of a software error being the main cause of an aircraft crash up to date, these systems also seem to be very reliable in practice. This success can at least partially be attributed to the aviation software certification process, which places a set of strict requirements on the system that must be taken into account during its development. One such requirement, applicable only to the most critical systems, is showing complete modified condition/decision coverage on the implementation of the system using tests generated from the system specification. Modified condition/decision coverage is a very demanding form of code coverage, whose purpose is to show both that sufficient testing has been performed to ensure correct operation, and that the implementation is correct in terms of the specification. As generating the tests by hand is very demanding, in terms of this work we study how automation can be used to facilitate this process. This thesis presents goal constraints, a novel extension to dynamic symbolic execution, which makes automatic generation of a set of tests satisfying modified condition/decision coverage possible. The goal constraints are essentially additional constraints on the values of variables instrumented into the program source code. They can be used during dynamic symbolic execution both to direct the testing process, and to select test cases based on the code coverage they provide. We present how goal constraints can be automatically generated and instrumented into the source code of a program written in the C programming language, and how support for goal constraints is implemented in an automated software testing tool called LIME Concolic Tester. The implementation is also evaluated, and the advantages and disadvantages of automated test generation in the context of aviation software development are discussed. en
dc.description.abstract Ohjelmistojärjestelmän oikean toiminnallisuuden varmistaminen on olennainen osa mitä tahansa ohjelmistokehitysprosessia, mutta erityisen tärkeää lentokoneissa käytettäville turvallisuuskriittisille järjestelmille, joissa ongelmilla voi olla vakavat seuraukset. Koska yksikään lentokone ei ole vielä toistaiseksi pudonnut virallisten lähteiden mukaan suoraan ohjelmistovirheen seurauksena, nämä järjestelmät vaikuttavat myös täyttävän niille asetetut luotettavuusvaatimukset erittäin hyvin. Hyvästä menestyksestä voidaan ainakin osittain kiittää lentokoneohjelmistojen kelpoistamisprosessia, joka määrittelee järjestelmille joukon tiukkoja vaatimuksia, jotka on otettava huomioon niiden kehityksen aikana. Yksi näistä vaatimuksista on täydellinen MC/DC-peittävyys järjestelmän toteutukselle käyttäen testejä, jotka on tuotettu järjestelmän määritelmästä. Tämä vaatimus koskee ainoastaan kaikista kriittisimpiä järjestelmiä, ja sen tarkoitus on osoittaa paitsi että toteutus on määritelmän mukainen, myös että toteutus ei sisällä ei-toivottua toiminnallisuutta. Koska MC/DC-testien tuottaminen käsin on hyvin työlästä, tutkimme tämän työn puitteissa miten automaatiota voidaan soveltaa helpottamaan tätä prosessia. Tämä työ esittelee tavoiterajoitteet, uuden laajennksen dynaamiselle symboliselle suoritukselle, joka mahdollistaa automaattisen MC/DC-testien tuottamisen. Tavoiterajoitteet ovat olennaisesti ohjelman lähdekoodiin lisättyjä lisävaatimuksia siinä esiintyvien muuttujien arvoille, ja niitä voidaan käyttää dynaamisen symbolisen suorituksen aikana sekä ohjaamaan testausta, että valitsemaan kiinnostavia testejä. Esitämme miten tavoiterajoitteet voidaan automaattisesti tuottaa ja instrumentoida C-kielisen ohjelman lähdekoodiin, ja miten tuki tavoiterajoitteille on toteutettu automaattiseen ohjelmistotestaustyökaluun nimeltä LIME Concolic Tester. Esitämme myös miten arvion toteutuksesta, ja keskustelemme mitä hyviä ja huonoja puolia liittyy automaattiseen ohjelmistotestaukseen lentokoneohjelmistojen kelpoistamisprosessin näkökulmasta. fi
dc.format.extent viii + 60 s.
dc.format.mimetype application/pdf
dc.language.iso en en
dc.title MC/DC Based Test Selection for Dynamic Symbolic Execution en
dc.title MC/DC-pohjainen testivalinta dynaamiselle symboliselle suoritukselle fi
dc.type G2 Pro gradu, diplomityö fi
dc.contributor.school Perustieteiden korkeakoulu fi
dc.contributor.school Perustieteiden korkeakoulu fi
dc.subject.keyword MC/DC fi
dc.subject.keyword DSE fi
dc.subject.keyword peittävyys fi
dc.subject.keyword automaattinen ohjelmistotestaus fi
dc.subject.keyword lähdekoodin instumentointi fi
dc.subject.keyword code coverage en
dc.subject.keyword automated software testing en
dc.subject.keyword source code instrumentation en
dc.identifier.urn URN:NBN:fi:aalto-201310307764
dc.type.dcmitype text en
dc.programme.major Tietojenkäsittelyteoria fi
dc.programme.mcode T-79
dc.type.ontasot Diplomityö fi
dc.type.ontasot Master's thesis en
dc.contributor.supervisor Heljanko, Keijo


Files in this item

This item appears in the following Collection(s)

Show simple item record

Search archive


Advanced Search

article-iconSubmit a publication

Browse

My Account