haku: @instructor Heljanko, Keijo / yhteensä: 44
viite: 19 / 44
| Tekijä: | Kauttio, Janne |
| Työn nimi: | MC/DC Based Test Selection for Dynamic Symbolic Execution |
| MC/DC-pohjainen testivalinta dynaamiselle symboliselle suoritukselle | |
| Julkaisutyyppi: | Diplomityö |
| Julkaisuvuosi: | 2013 |
| Sivut: | viii + 60 Kieli: eng |
| Koulu/Laitos/Osasto: | Perustieteiden korkeakoulu |
| Oppiaine: | Tietojenkäsittelyteoria (T-79) |
| Valvoja: | Heljanko, Keijo |
| Ohjaaja: | Heljanko, Keijo |
| Elektroninen julkaisu: | http://urn.fi/URN:NBN:fi:aalto-201310307764 |
| OEVS: | Sähköinen arkistokappale on luettavissa Aalto Thesis Databasen kautta.
Ohje Digitaalisten opinnäytteiden lukeminen Aalto-yliopiston Harald Herlin -oppimiskeskuksen suljetussa verkossaOppimiskeskuksen 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
Opinnäytteen avaaminen
Opinnäytteen lukeminen
Opinnäytteen tulostus
|
| Sijainti: | P1 Ark Aalto | Arkisto |
| Avainsanat: | code coverage automated software testing source code instrumentation MC/DC DSE peittävyys automaattinen ohjelmistotestaus lähdekoodin instumentointi |
| Tiivistelmä (fin): | 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. |
| Tiivistelmä (eng): | 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. |
| ED: | 2013-10-28 |
INSSI tietueen numero: 47405
+ lisää koriin
INSSI