Ekvivalenciapartíciók meghatározása C programokban szimbolikus végrehajtással

Életünk minden területén egyre nagyobb szerep hárul a szoftverekre. Ez biztonságkritikus területeken sincs másképp: többek között az autóipar és a repülőgépipar is egyre inkább szoftver-orientált. Fontos, hogy ezen iparágak termékei biztonságosak legyenek, hisz működésükön akár emberéletek is múlhatnak.

A magas fokú biztonság elérésének érdekében a fejlesztőknek meg kell győződniük arról, hogy az elkészített szoftver helyesen működik minden bemenetre. Ezeknek a – főleg beágyazott – szoftvereknek a komplexitása azonban elég magas, így közel lehetetlen az elkészült programot minden lehetséges bemenetre tesztelni. Egy megoldás lehet erre a problémára, hogy osztályozzuk a bemeneteket aszerint, hogy mely értékekre viselkedik a program közel azonosan: vagyis bontsuk a bemeneteket ekvivalenciapartíciókra. Ezeknek az osztályoknak a meghatározása segíthet feltárni a redundáns teszteket, illetve fontos, még le nem fedett eseteket. Munkánk célja tehát egy olyan alkalmazás létrehozása, mellyel képesek leszünk a forráskódot vizsgálva automatikusan meghatározni ezeket az ekvivalenciapartíciókat, elősegítve a minél jobb minőségű teszthalmaz megírását.

Munkánk során a Klee nevű szimbolikus végrehajtót használtuk, amely képes felfedni számunkra a program legtöbb futási útját, ezzel magasfokú kódlefedettséget biztosítva. Emellett az egyes utakhoz olyan bemeneteket is biztosít, amikkel a program újbóli futtatása során ugyanazt az utat járhatjuk be. Bár az utakat és a hozzájuk tartozó bemeneteket megadja a Klee, kihívást jelent az ekvivalenciapartíciók konkrét meghatározása. Dolgozatunk során két megoldási módszert mutatunk be.

Az egyik módszer során a Klee által meghatározott bemenetekkel futtatjuk a programot. A futás után a forráskód lefedettségét megvizsgálva megkaphatjuk a konkrét bejárt utakat. Innen kinyerhetőek a bejárt út során teljesülő feltételek, amiket egyszerűsítve és összegezve meghatározható egy-egy ekvivalenciapartíció. A fő kihívást ebben a módszerben az jelenti, hogy a megkapott feltételek által tartalmazott köztes változókat és függvényhívásokat kiküszöböljük.

A másik módszer során azt használjuk ki, hogy a Klee az egyes utakon összegyűjti a kényszereket, hogy azok megoldásával (SMT megoldó segítségével) bemenetet generálhasson az adott útra. A fő kihívás ebben a megközelítésben az, hogy a Klee LLVM byte kódon dolgozik a C forráskód helyett. Tehát, amikor a lekérdezéseket vizsgáljuk, át kell hidalni az absztrakciós szintek közötti távolságot, amely az alacsony szintű byte kód és a C forráskód között van, illetve helyre kell állítanunk az elveszett típus információkat is, amelyek szükségesek az ekvivalenciapartíciók meghatározásához.

A célunk egy olyan eszköz elkészítése, amely mindkét módszert tudja alkalmazni, hisz ezek kiegészítik egymást, és más-más esetekben alkalmazhatók. Az eszköz segítségével a fejlesztők képesek lesznek jobban belelátni a szoftver működésébe az ekvivalenciapartíciók által. A követelmények és a kapott ekvivalenciapartíciók alapján javítani tudják a meglévő tesztkészületük hatékonyságát.

szerzők

Kubriczky Ádám
Mérnök informatikus szak, alapképzés
alapképzés (BA/BSc)
Tóth Nikolett
Mérnök informatikus szak, mesterképzés
mesterképzés (MA/MSc)

konzulensek

Dr. Micskei Zoltán
egyetemi docens, Mesterséges Intelligencia és Rendszertervezés Tanszék
Dr. Vörös András
egyetemi docens, Mesterséges Intelligencia és Rendszertervezés Tanszék